실시간 모델 체커를 이용한 월성 SDS2의 명세 및 검증 = Specifying and Verifying Wolsong SDS2 Using Real - Time Model Checker

국문 초록 (Abstract)

실시간 시스템은 그 특성상 시스템 내에서의 오류가 매우 위험하고 때론 치명적일 수 있다. 따라서, 시스템의 정확성과 안정성을 보장하는 것은 매우 중요한 문제가 된다. 이러한 문제를 해결하기 위해 정형기법을 사용한 명세와 검증을 통해 실시간 시스템의 안정성을 보장하려는 시도들이 많이 이루어져 왔다. 이 논문에서는 월성 원자로 운전 중지 시스템의 기존 명세의 문제점을 보완하여, 실시간 요구사항들을 타임드 오토마타(timed automata)로 기술할 것을 제안한다. 또한 명세를 실시간 모델 체커 UPPAAL의 입력으로 넣어서, 모델 체킹 기법을 이용해 자동적으로 시간 제약 속성을 검증한다.

목차 (Table of Contents)

• 요약
• 1. 서론
• 2. 예제 : 월성 제2원자로 운정 중지기
• 3. 실시간 모델체커를 이용한 명세 및 검증
• 4. 결론
• 참고문헌