Title: A methodological approach for checking safety-critical systems software
Authors: Luis E. Mendoza; Manuel I. Capel
Addresses: Facultad de Ingeniería en Electricidad y Computación, Campus Gustavo Galindo Km 30.5 Vía Perimetral, Escuela Superior Politécnica del Litoral, ESPOL, P.O. Box 09-01-5863, Guayaquil, Ecuador; Processes and Systems Department, Simón Bolívar University, USB, P.O. box 89000, Baruta, Caracas 1080-A, Venezuela ' ETSI Informatics and Telecommunication, Software Engineering Department, University of Granada, UGR, 18071 Granada, Spain
Abstract: 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.
Keywords: critical computer-based systems; methodological approach; safety-critical systems software; model checking; software verification; software specification; compositional verification.
DOI: 10.1504/IJCCBS.2017.089985
International Journal of Critical Computer-Based Systems, 2017 Vol.7 No.4, pp.341 - 368
Received: 15 Jun 2016
Accepted: 21 Aug 2017
Published online: 26 Feb 2018 *