LUSTRE 를 이용한 SCR 명세의 구현 = Implementing SCR Specification with LUSTRE

국문 초록 (Abstract)

SCR 방법론은 고 신뢰도를 요구하는 시스템 개발을 위해 사용되는 요구사항의 정형적 명세의 하나로, 오랜 역사와 많은 응용 사례를 가지고 있다. 이 방법론에 따라 사용자가 요구사항을 명세했을 때 그것을 어떻게 정확하게 구현할 수 있는지가 중요한 문제가 된다. 본 논문에서는 SCR로 작성된 명세를 그 의미를 보전하는 구현언어로 자동으로 변환시키는 방법을 제시한다. SCR 명세가 가지는 자료흐름 언어와의 유사성을 이용하기 위해, 구현언어로 동기적 자료흐름 언어인 LUSTRE를 선택했고, 그 변환 과정을 제시하였다. 제안한 방법의 유용성을 살피기 위해, SCR과 유사한 방법으로 작성된 월성 원자력 발전소의 제 2 정지 시스템의 일부분을 변환하는 실험을 수행, 그 결과를 비교하였다. 정형명세가 도입되어서 사용될 경우, 본 연구는 개발의 전체 소요시간을 줄여줄 수 있고 좀더 신뢰성있는 결과물을 내는데 도움을 줄 수 있다.

다국어 초록 (Multilingual Abstract)

Formal specification and verification of software requirements is now gaining popularity in the field of safety-critical embedded systems. SCR (Software Cost Reduction) is one of such formal methods that has been applied to several real-world projects. We propose a procedure that translates an SCR specification into an executable program written in the sequential implementation language, such as C. We exploit the similarity between basic semantic models of SCR and the synchronous data-flow langauge LUSTRE. An SCR specification can be translated into a LUSTRE program of same meaning, and then, existing LUSTRE compiler can produce a sequential code. The correctness of our method is explained based on the formal semantics of SCR. To demonstrate the practicality of the method, a small portion of the requirement specification of Wolsung shutdown system 2, which is specified in SCR-like method, is translated into LUSTRE. We compare the result with the original code, and give some evidence of the practicality. This method may reduce the development time and increase the reliability of the final product when applied to the formal specification.

목차 (Table of Contents)

• 요약
• Abstract
• 1. 서론
• 2. 배경 연구
• 3. SCR 언어의 LUSTRE 언어로의 변환
• 4. Case Study : 월성 원자로 SDS2
• 5. 결론
• 참고문헌
• 부록
• 저자소개