Article: A methodological approach for checking safety-critical systems software Journal: International Journal of Critical Computer-Based Systems (IJCCBS) 2017 Vol.7 No.4 pp.341 - 368 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. Inderscience Publishers - linking academia, business and industry through research

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

Accepted: 21 Aug 2017
Published online: 26 Feb 2018 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article

Title: A methodological approach for checking safety-critical systems software

Keep up-to-date