안전 필수 철도 시스템 개발을 위한 요구 사항의 정형 명세 작성 = Development of the Formal Requirements Specification of the Safety-critical Railway Systems

국문 초록 (Abstract)

철도 제어 시스템은 대표적인 안전필수 시스템이다. 국제 규격의 컴퓨터 기반의 철도 제어 시스템을 개발하기 위해서 정형 기법을 이용한 요구사항 명세와 검증이 요구된다. 본 논문에서는 정형 기법을 사용하여 요구사항 명세를 작성하는 지침서(guideline)을 개발하고, 컴퓨터 기반의 열차 제어 장치 시스템에 대한 실제 적용 사례를 제시한다. 정형 명세를 위해 상태차트(statechart)와 Z를 사용하고, 정형 명세의 일치성(consistency)과 완전성(completeness)을 검증한다.

다국어 초록 (Multilingual Abstract)

A railway control system is one of the typical safety-critical systems. It is required to use formal methods for the requirements specification and verification in order to develop the global-standard railway control systems based on the computer systems. In this paper, we develop a guideline for requirements specification using formal methods, and present a case study of the development of a computer-based railway control system through the application of the proposed guideline. We use the Statechart and the Z method for the formal requirements specifications and verify the consistency and completeness of the formal specifications of the requirements.

목차 (Table of Contents)

• 요약
• Abstract
• 1. 서론
• 2. 관련 연구
• 3. 철도 시스템을 위한 정형 요구사항 명세 지침서
• 4. 정형 명세 기법의 적용
• 5. 분석
• 6. 결론
• 참고문헌

참고문헌 (Reference)

1 Janota, A.:, "Using Z specification for railway interlocking safety" 28 (28): 39-53, 2000

2 Monin,J-F, "Understanding Formal Methods" Springer-Verlag 2003

3 Zowghi, D, "The three Cs of Requirements: Consistency, completeness, and Correctness, Proc" 2002

4 Grady, J, "System Requirements Analysis" Elsevier 2006

5 Bjorner, D., "Software Engineering" Springer 2006

6 Hull, E, "Requirements Engineering" Springer 2005

7 Hartley, D., "Process for System Architecture and Requirements Engineering" Dorset House 2000

8 Harel,D, "On Visual Formalisms" 31 (31): 514-530, 1988

9 Horste, M.M, "Modelling and simulation of train control systems using Petri nets" Springer-Verlag 720-, 1999

10 Harel, D, "Modeling Reactive Systems with Statescharts" McGraw-Hill 1998

11 Cimatti A., "Model Checking safety critical software with SPIN: an Application to a Railway Interlocking System, SAFECOMP, LNCS 1516" Springer-Verlag 284-293, 1998

12 Potter, B, "Introduction to Formal Specification and Z" Prentice-Hall 1996

13 "IEEE Std. 830, "IEEE Recommended Practice for Software Requirements Specifications,""

14 "IEEE Std. 1233, "IEEE Guide for Developing System Requirements Specifications,""

15 "IEEE Std 1474.1-2004, "Standard for Communications-Based Train Control Performance and Functional Requirements""

16 "IEEE Std 12207, "Standard for Information Technology–Software life cycle processes,""

17 "IEC Std. 62425, "Railway applications-Communication, signaling and processing systems–safety- related electronic systems for signaling,""

18 "IEC Std. 62280, "Railway applications-Communication, signaling and processing systems,""

19 "IEC Std. 62279, "Railway applications-Software for railway control and protection systems,""

20 "IEC Std. 62278, "Railway applications-Specification and demonstration of reliability," availability, maintainability and safety(RAMS)"

21 "IEC Std. 61508, "Functional safety of electrical/ electronic/programmable electronic safety-related systems,""

22 Bowen, J, "Formal methods in safety-critical standards" 168-177, 1993

23 Clarke, E.M, "Formal Methods: State of the Art and Future Directions" ACM Computing Surveys 1996

24 Lecomte, T., "Formal Methods in safety-critical railway system" 2007

25 Abdulla, P.A., "Designing Safe" Reliable systems using SCADE 115-129, 2006