Correctness by construction 기반 안전 필수 Ada 프로그램 연구

국문 초록 (Abstract)

정보혁명이 시작된 이후 컴퓨터 시스템은 우리생활의 곳곳에서 사용되며 인간에게 많은 편리함을 제공하고 있다. 높은 기능성에 대한 요구사항 때문에 컴퓨터시스템이 복잡해짐에 따라 시스템 내부의 치명적인 오류의 잠재성도 증가했다. 오류로 인한 기능실패로 재산적, 인명적인 피해를 초래할 수 있는 시스템을 안전필수시스템이라고 한다. 안전필수시스템을 개발할 때는 정확성(Correctness)과 고 무결성(High-Integrity)을 보증하는 것이 중요하다.
시스템 개발 초기부터 시스템의 정확성과 고 무결성을 보증하기 위한 개발방법으로 Correctness by Construction이 있다. Correctness by Construction은 정확성을 보증하기 위한 정형기법과 생산성을 높이기 위한 애자일 방법론이 결합된 방법이다. 이 방법은 영국의 Praxis사에서 처음 제안했으며 많은 사례연구를 통해 그 유용성이 알려져 있다.
하지만 기존 Correctness by Construction의 프로세스로는 제어정보를 표현하기가 힘들기 때문에 반응형 시스템과 같이 제어부분이 중요한 시스템들은 Correctness by Construction 개발 방법을 적용하기가 쉽지 않다. 따라서 Correctness by Construction 개발 방법에 제어 정보를 표현하는 명세 및 코드를 도출하는 프로세스가 필요하다
본 논문에서는 Correctness by Construction프로세스에 컨트롤을 명세, 개발하는 프로세스를 추가하여 개선된 Correctness by Construction 프로세스를 제안한다. 또한 개선된 Correctness by Construction 개발방법을 거리제어모듈 개발에 적용한 사례연구를 수행한다. 거리제어모듈은 철도제어시스템 중 열차의 간격을 제어하는 모듈로서 안전필수시스템이다. 이 사례연구의 결과를 통해 정확성과 고 무결성을 가지는 안전필수시스템의 개발가이드를 제안한다.

목차 (Table of Contents)

• 1. 서 론 1
• 2. 관련연구 4
• 2.1. Z notation 4
• 2.2. Spark 5
• 3. Correctness by Construction 7
• 3.1. 정형기법 7
• 3.1.1. 정형 명세 7
• 3.1.2. 정형 검증 7
• 3.2. 애자일 개발 방법 8
• 3.3. Correctness by Construction 소개 8
• 3.3.1. Correctness by Construction의 기본 원리 9
• 3.3.2. Building Blocks 9
• 3.3.3. Core Process 12
• 3.4. Tokeneer ID Station 프로젝트 18
• 3.4.1. Tokeneer 시스템 18
• 3.4.2. Tokeneer ID Station프로젝트 결과 19
• 4. 한계 및 개선방안 20
• 4.1. ACC(감응순항제어장치) 예제 22
• 4.1.1. ACC 상태 스키마 23
• 4.1.2. ACC 오퍼레이션 스키마 25
• 4.1.3. ACC Statechart 명세 26
• 5. 거리제어모듈 소개 29
• 5.1. Mock-Up 열차 제어 시스템 구성 29
• 5.1.1. 전체구성 30
• 5.2. 거리제어모듈 32
• 5.2.1. 거리제어모듈 기능 33
• 6. 사례연구: Correctness by Costruction를 적용한 DCM개발 43
• 6.1. Software Specification 43
• 6.2. Specification Verification 48
• 6.2.1. 초기 모델에 대한 일관성 검증 48
• 6.2.2. 오퍼레이션에 대한 일관성 검증 48
• 6.2.3. 오퍼레이션에 대한 완전성 검증 49
• 6.3. Statechart 명세 50
• 6.4. Spark Specification 52
• 6.5. Spark Body Code 54
• 6.6. Code Verification 57
• 7. 결론 61
• 8. 참고문헌 63