Building Models We Can Rely On: Requirements Traceability for Model-Based Verification Techniques

摘要

Proving the safety of a critical system is a complex and complicated task. Model-based formal verification techniques can help to verify a System Requirement Specification (SRS) with respect to normative and safety requirements. Due to an early application of these methods, it is possible to reduce the risk of high costs caused by unexpected, late system adjustments. Nevertheless, they are still rarely used. One reason among others is the lack of an applicable integration method in an existing development process. In this paper, we propose a process to integrate formal model-based verification techniques into the development life-cycle of a safety critical system. The core idea is to systematically refine informal specifications by (1) categorization, (2) structural refinement, (3) expected behavioral refinement, and finally, (4) operational semantics. To support modeling, traceability is upheld through all refinement steps and a number of consistency checks are introduced. The proposed process has been jointly developed with the German Railroad Authority (EBA) and an accredited safety assessor. We implemented an Eclipse-based IDE with connections to requirement and systems engineering tools as well as various verification engines. The applicability of our approach is demonstrated via an industrial-sized case study in the context of the European Train Control System with ETCS Level 1 Pull Supervision.