초록 ▼

연구개요
CPS는 소프트웨어를 활용하여 물리적 개체를 제어하는 컴퓨터 시스템을 의미하며, 높은 안전성과 신뢰성을 보장하기 위한 CPS 소프트웨어 검증 기술이 매우 중요하다.
모델검증은 소프트웨어가 주어진 요구사항을 만족하는지 알고리즘적으로 검증하는 자동 정형 검증 기술이다. 과거 모델검증은 이산적(discrete) 소프트웨어 분석 위주로 개발되었으나, 최근 연속적인(continuous) 물리적 개체를 고려한 CPS 모델검증 기술이 활발히 연구되고 있다. 하지만 기존 모델검증 기술은 이산적인 코드와 연속적인 물리환경을 동시

연구개요
CPS는 소프트웨어를 활용하여 물리적 개체를 제어하는 컴퓨터 시스템을 의미하며, 높은 안전성과 신뢰성을 보장하기 위한 CPS 소프트웨어 검증 기술이 매우 중요하다.
모델검증은 소프트웨어가 주어진 요구사항을 만족하는지 알고리즘적으로 검증하는 자동 정형 검증 기술이다. 과거 모델검증은 이산적(discrete) 소프트웨어 분석 위주로 개발되었으나, 최근 연속적인(continuous) 물리적 개체를 고려한 CPS 모델검증 기술이 활발히 연구되고 있다. 하지만 기존 모델검증 기술은 이산적인 코드와 연속적인 물리환경을 동시에 고려해야 하는 어려움으로, 단순화된 설계 수준에서 수행하는 시각에 머무르고 있다. CPS 소프트웨어가 설계 수준에서는 올바르더라도 실제 구현 코드에 존재하는 프로그램의 오류로 요구사항을 만족하지 않을 수 있으므로, 코드 수준에서 수행 가능한 정형검증 기술이 반드시 필요하다. 본 연구에서는, 기존 설계 수준 CPS 모델검증 기술의 한계를 극복할 수 있도록, CPS 소프트웨어의 요구사항을 자동으로 코드 수준에서 검증하기 위한 새로운 모델검증 기술을 개발하고, 실제적인 CPS 사례 연구를 통해서 제안한 기술의 효용성을 평가한다.

연구 목표대비 연구결과
본 연구의 최종 목표인 CPS 소프트웨어의 코드 수준 모델검증 기술을 개발하기 위해 본 연구에서는 다음의 3가지 세부 연구 내용을 수행한다.
* 세부연구1: 물리적 개체를 고려한 CPS 프로그래밍 언어의 의미구조 정의
-목표: CPS 프로그래밍 언어의 의미구조를 물리 환경을 고려하여 새롭게 정의하여 CPS 소프트웨어의 코드 수준 정형 검증을 위한 논리적 토대를 제공
-결과: 변수, 할당, 분기, 반복, 함수 등 명령형 프로그래밍 언어의 특징을 포함하고, 시간에 따라 변하는 물리적 변수를 포함하는 언어와 의미구조 정의로 목표 달성
* 세부연구2: 효율적인 코드 수준 모델검증 알고리즘 연구
-목표: CPS 프로그래밍 언어의 의미구조 정형명세를 활용하여 해당 언어로 작성된 프로그램에 대한 효과적인 모델검증 알고리즘 및 성능최적화 기술을 연구
-결과: Rewriting modulo SMT을 기반으로, CPS의 연속적 시간 및 분산 시스템의 특징에 최적화된 모델검증 알고리즘 및 상태 공간 축소 기술 개발로 목표 달성
* 세부연구3: 무인항공기 제어 소프트웨어의 코드 수준 모델검증 사례연구
-목표: 다수의 무인항공기를 제어하여 충돌을 방지하는 분산 CPS 알고리즘 코드에 대한 모델검증을 수행하는 사례연구 수행
-결과: 기존 기술로는 검증이 매우 어려웠던 두 종류의 코드 수준 무인항공기 제어 프로그램에 대한 모델검증 사례연구를 성공적으로 수행하여 목표 달성

연구개발성과의 활용 계획 및 기대효과 (연구개발결과의 중요성)
-기존의 “설계 수준 CPS 모델검증 연구 패러다임에서 벗어나는, CPS 소프트웨어를 위한 코드 수준 모델검증 기술을 최초로 개발하여 원천기술 및 연구기반 확보
-기존 연구에서 거의 시도되지 않았던, CPS의 물리 환경, 코드 수준의 정밀성, 높은 검증 효율성을 모두 달성하는 도전적인 문제에 대한 새로운 접근방법을 제시
- 자율주행차량 등의 핵심 소프트웨어 개발에 필수적인 CPS 소프트웨어 검증 기술을 개발하여, 기존 선진국 위주의 산업에 국내 기술로 진입할 수 있는 디딤돌 제공
- 산업체에서 CPS 소프트웨어의 코드 수준 검증 기술 활용을 통해, 개발자의 생산성 향상, 기업의 유지보수 비용 절감, 나아가 제품의 품질 향상 및 경쟁력 향상에 기여

(출처 : 요약문 2p)

목차 Contents

• 표지 ... 1
• 연구결과 요약문 ... 2
• 목차 ... 3
• 1. 연구개발과제의 개요 ... 4
• 1) 연구배경 ... 4
• 2) 기존 CPS 소프트웨어 모델검증 기술의 한계 ... 4
• 3) CPS 소프트웨어를 위한 코드 수준 정형 검증 기술의 필요성 ... 5
• 4) 연구 목표 ... 5
• 4) 연구 범위 ... 5
• 2. 연구개발과제의 수행 과정 및 수행 내용 ... 6
• 1) 세부연구내용1: 물리적 개체를 고려한 CPS 프로그래밍 언어의 의미구조 정의 ... 6
• 2) 세부연구내용2: CPS 소프트웨어의 효율적인 코드 수준 모델검증 알고리즘 연구 ... 9
• 3) 세부연구내용3: 무인항공기 제어 소프트웨어의 코드 수준 모델검증 사례연구 ... 11
• 3. 연구개발과제의 수행 결과 및 목표 달성 수준 ... 13
• 1) 정성적 연구개발성과(연구개발결과) ... 13
• 2) 세부 정량적 연구개발성과 ... 13
• 3) 목표 달성 수준 ... 14
• 4. 연구개발성과의 관련 분야에 대한 기여 정도(연구개발결과의 중요성) ... 14
• 1) 연구 분야의 파급효과 ... 14
• 2) 산업 분야의 파급효과 ... 14
• 5. 연구개발성과의 관리 및 활용 계획 ... 14
• 1) 추가 연구의 필요성: 코드를 생성하는 모델 기반 CPS 소프트웨어 개발 기술 ... 14
• 2) 연구개발결과의 활용계획 ... 15
• 6. 자체점검표 ... 15
• 7. 참고문헌 ... 15
• [붙임1] 세부 정량적 연구개발성과 ... 19
• [붙임2] 연구책임자 대표적 연구실적 및 증빙(요약문 및 사본) ... 21
• 끝페이지 ... 32