Application of Architectural Patterns and Lightweight Formal Method for the Validation and Verification of Safety Critical Systems

This thesis researches the role of software architectural patterns and lightweight formal methods in safety-critical software development. We present a framework that relates the different activities and products from system engineering, safety engineering, system and software requirements, and software architecture explicitly, and demonstrate the proposed framework with a case study involving the architectural design of the software to control the arming device of a fictitious Surface-to-Air Missile. We describe the safety engineering steps for the identification of the system hazards and the critical functions that the software has to provide to avoid premature detonation, resulting in four safety requirements for the software that controls the missile's Electronic Safe Arm Device (ESAD). We formalize the software safety requirements as statechart assertions and validate their correctness via JUnit test. We develop a software architecture for the control software using the Safety Executive pattern, and implement the design in C++ to support a simple time-step simulation to produce the required log files for the automated verification of the design.