초록 ▼

연구개요
CPS는 소프트웨어를 이용하여 물리 개체를 제어하는 분산 컴퓨터 시스템을 의미하며, 자율주행자동차, 무인항공기, 스마트 공장 등을 위한 소프트웨어를 예로 들 수 있다.
CPS는 물리 세계와 상호작용을 하기 때문에, CPS의 안전성/신뢰성 요구사항은 종종 연속적으로 변하는 물리적 개체의 상태와 연관되어 있으며, Signal temporal logic은 연속적인 상태 변화를 포함하는 CPS 소프트웨어의 요구사항을 엄밀히 표현하기 위해 사용되는 시제 논리 언어이다. 모델검증은 소프트웨어의 모델이나 코드가 주어진 논리적

연구개요
CPS는 소프트웨어를 이용하여 물리 개체를 제어하는 분산 컴퓨터 시스템을 의미하며, 자율주행자동차, 무인항공기, 스마트 공장 등을 위한 소프트웨어를 예로 들 수 있다.
CPS는 물리 세계와 상호작용을 하기 때문에, CPS의 안전성/신뢰성 요구사항은 종종 연속적으로 변하는 물리적 개체의 상태와 연관되어 있으며, Signal temporal logic은 연속적인 상태 변화를 포함하는 CPS 소프트웨어의 요구사항을 엄밀히 표현하기 위해 사용되는 시제 논리 언어이다. 모델검증은 소프트웨어의 모델이나 코드가 주어진 논리적 요구사항을 만족하는지를 알고리즘적으로 검증하는 기술이다. 기존 모델검증 기술은 이산적인 소프트웨어의 분석에 초점을 맞추고 있기 때문에, 연속적으로 상태가 변하는 물리적 개체를 제어하는 CPS 소프트웨어의 검증에는 매우 제한적이다. 본 연구에서는 STL 요구사항을 자동으로 검증하기 위한 효율적인 모델검증 알고리즘을 연구하고, 이를 이용하여 CPS 소프트웨어의 논리적 요구사항 검증 도구를 개발하는 것이다.

연구 목표대비 연구결과
본 연구의 대표 결과물은 CPS 소프트웨어의 STL 모델검증 도구이며, 이 연구 목표를 달성하기 위하여 3개의 세부연구로 구성되며, 목표와 결과는 다음과 같다.
* 세부연구1: 효율적인 STL 모델검증 알고리즘 개발
- 목표: 선행연구에서 개발된 기존 CPS 소프트웨어 STL 모델검증 알고리즘의 성능과 범위를 크게 향상시키는 알고리즘을 개발
- 결과: 시그널 이산화, Two-stel solving 등 복잡도 단순화를 통해 기존 알고리즘의 성능을 크게 향상시키는 새로운 STL 모델검증 알고리즘을 개발하여 목표를 달성
* 세부연구2: 분산 CPS를 위한 모델검증 알고리즘 개발
- 목표: 분산 CPS 소프트웨어를 위한 Rewriting/SMT 기반 효과적 모델검증 알고리즘 및 설계/검증 복잡도 단순화 기술을 개발
- 결과: 분산 CPS의 검증 복잡도 단순화를 위한 MSYNC를 개발하고, Rewriting/SMT 기술 기반 분산 CPS 모델검증 알고리즘을 개발하여 목표를 달성
* 세부연구3: CPS 소프트웨어의 모델검증 도구 개발
- 목표: 위의 기술들을 구현하는 효과적인 모델검증 도구를 개발하고, 벤치마크 평가를 통하여 성능과 효용성을 극대화한다.
- 결과: STL 모델검증 알고리즘을 구현하는 STLmc 모델검증 도구를 개발하고, 분산 CPS 검증 알고리즘을 HybridSynchAADL 도구에 개발하여 목표를 달성

연구개발성과의 활용 계획 및 기대효과 (연구개발결과의 중요성)
- CPS 소프트웨어의 효율적인 STL 모델검증 알고리즘과 도구를 세계 최초로 개발하여 CPS 소프트웨어 검증 분야를 선도
- 수작업으로 테스트 입력 시그널 생성과 검사를 반복하는, 과거 trial-and-error 기반 노동집약적 방법을 벗어나, STL 요구사항을 자동으로 검증하는 새로운 관점 제시
- 자율주행차량 등의 핵심 소프트웨어 개발에 필수적인 CPS 소프트웨어 검증 기술을 개발하여, 기존 선진국 위주의 산업에 국내 기술로 진입할 수 있는 디딤돌 제공
- 산업체에서 CPS 소프트웨어 검증 도구 활용을 통해, 개발자의 생산성 향상, 기업의 유지보수 비용 절감, 나아가 제품의 품질 향상 및 경쟁력 향상에 기여

(출처 : 요약문 2p)

목차 Contents

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