A Formal Compositional Verification Approach for Safety-Critical Systems Correctness: Model-Checking based Methodological Approach to Automatically Verify Safety Critical Systems Software

摘要

The complexity of modern Safety-Critical Systems (SCS) together with the absence of appropriate software verification tools is one reason for the large number of errors in the design and implementation of these systems. Moreover, exhaustive testing is hard and highly complex because of the combinatorial explosion in the great number of states that an SCS can reach when it executes. A methodological approach named FCVA that uses Model-Checking (MC) techniques to automatically verify SCS software is presented here. This approach facilitates decomposition of complex SCS software into independently verified individual components, and establishes a compositional method to verify these systems using state-of-the-art MC tools. Our objective in this paper is to facilitate the description of an SCS as a collection of verified components, allowing complete complex SCS software verification. An application on a real-life project in the field of mobile phone communication is discussed to demonstrate the applicability of FCVA.