An Operational Semantics for Simulating NuSCR Formal Specifications = NuSCR 정형 명세의 시뮬레이션을 위한 동작 시맨틱

다국어 초록 (Multilingual Abstract)

Rigorous verification & validation of software through formal method is highly recommended when developing a safety critical system like a digital protection system in a nuclear power plant (NPP). Various formal specification-based verification techniques, such as testing, simulation and model checking, have been proposed to verify and validate the specifications. This paper describes the foundation and tool to support simulation of the software requirements written in NuSCR formal specification language. We have defined an operational semantics for NuSCR language based in natural semantics and simulation engine algorithms for NuSCR Software System (NSS) which is a symbolic executable model of the software system written in NuSCR. The operational semantics and simulation engine algorithms have been implemented as a simulator – “NuSCRSim”. It provides an visual animation of the NuSCR constructs, which makes it easier to directly check the behavior of a model. We also performed a case study with examples of the APR-1400 nuclear reactor protection system in Korea in order to demonstrate of the correctness of the “NuSCRSim”.

국문 초록 (Abstract)

원자력 발전소의 디지털 보호 시스템과 같이 안전 필수 시스템에 들어가는 소프트웨어를 개발할 때는 정형 기법을 통한 소프트어의 엄격한 검증 및 확인이 권장된다. 이에 따라, 요구사항 단계에서 테스트, 시뮬레이션 및 모델 체킹과 같은 다양한 정형 명세 기반 검증 기술이 제안되었다. 본 논문에서는 NuSCR 정형 명세 언어로 작성된 소프트웨어 요구 사항의 시뮬레이션을 지원하기 위한 기초이론과 이론을 구현한 시뮬레이터 도구를 제안한다. 먼저 시뮬레이션을 하기 위한 기반이론이 되는 NuSCR 언어의 동작 시맨틱을 Natural Semantic 방법을 기반으로 정의하였고 NuSCR로 작성된 소프트웨어 시스템의 실행 모델인 NSS (NuSCR 소프트웨어 시스템)의 특성에 맞춰 시뮬레이션 엔진을 정의하였다. 해당 동작 시맨틱 및 시뮬레이션 엔진은 NuSCR로 작성된 정형 명세를 시뮬레이션 할 수 있는 시뮬레이터인 “NuSCRSim” 으로 구현되었다. 해당 도구는 NuSCR 구조의 시각적인 애니메이션을 제공하여 모델의 동작을 쉽게 이해할 수 있게 도와준다. 우리는 또한 해당 시뮬레이터의 정확성을 입증하기 위해 APR-1400 원자로 보호 시스템의 하나의 모듈을 이용하여 시험을 수행하였다.

목차 (Table of Contents)

• Chapter 1. Introduction 1
• Chapter 2. Background 4
• 2.1. NuSCR 4
• 2.2. Discrete Time Models and Simulations 6
• 2.3. Operational Semantics 8
• Chapter 3. The foundation for Simulating NuSCR Specification 11
• 3.1. Operational Semantics for NuSCR 11
• 3.1.1 Run of a NuSCR Software System 12
• 3.1.2 Operational Semantics for FOD 13
• 3.1.3 Operational Semantics for SDT 15
• 3.1.4 Operational Semantics for FSM 16
• 3.1.5 Operational Semantics for TTS 17
• 3.2. Simulation Engines for NuSCR Software System 19
• Chapter 4. NuSCRSim 21
• Chapter 5. Case Study 23
• 5.1. An Overview of the Target Module 24
• 5.2. Preparation 25
• 5.3. Evaluation 26
• Chapter 6. Related Work 30
• Chapter 7. Conclusion and Future Work 33
• References 34
• Abstract (in Korean) 40