A methodological approach for checking safety-critical systems software.

The complexity of modern safety-critical systems 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. A methodological approach named formal compositional verification approach that uses model checking techniques to verify safety-critical systems software is presented. This approach facilitates decomposition of complex safety-critical systems software into independently verified individual software components, and establishes a compositional method to verify these systems using state-of-the-art model checkers. Our objective in this paper is to facilitate the description of a safety-critical system software as a collection of verified software components, allowing the software verification of complex safety-critical systems. An application on a real-life software project in the field of mobile phone communication is discussed to demonstrate the applicability of the proposed approach.