유도조종장치는 안전성이 중요한 시간 기반 내장형 시스템이며 유도조종장치 소프트웨어의 시간 제약성 만족은 소프트웨어 안전성 확보를 위한 매우 중요한 문제이다. 기존 유도조종장치 소프트웨어 개발에서는 주로 테스트 단계의 시뮬레이션 기법을 통해 시간 제약성 만족을 확인한다. 하지만 시뮬레이션 환경을 구축하기 위한 추가적인 시간과 노력이 소요될 뿐만 아니라 시간 관련 오류의 개발 후 발견은 소프트웨어 안전성을 저하시키며, 전체 소프트웨어 개발 비용을 증가시킬 수 있다. 이러한 단점을 보완하기 위해 본 논문에서는 설계 단계에 모델 체킹 기법을 적용하여 유도조종장치 소프트웨어의 시간 제약성을 검증하고자 한다. 이를 위해서 실시간 시스템에 대한 모델링과 검증을 지원하는 TIMES 도구를 유도조종 장치 소프트웨어 설계에 적용하는 사례 연구를 수행하고 그 결과를 분석 및 평가하였다.
Guidance and Control Unit (GCU) is a safety-critical and time-triggered embedded system and it is crucial to satisfy with timing constraints of GCU software to increase software safety. Usually timing constraints of GCU software are validated with a simulation method in test phase. However, constructing simulation environments needs to invest much time and effort. Furthermore, detecting errors in later phases can lead to a development cost increase. To compensate these drawbacks, a model checking method can be applied to validate timing constraints of GCU software in design phase. To this end, we accomplish a case study on validating GCU software using TIMES model checking tool, and evaluate results of the case study.
