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

Manuel I. Capel, Luis E. Mendoza Morales

2012

Abstract

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.

Paper Citation

in Harvard Style

I. Capel M. and E. Mendoza Morales L. (2012). A Formal Compositional Verification Approach for Safety–Critical Systems Correctness - Model–Checking based Methodological Approach to Automatically Verify Safety Critical Systems Software . In Proceedings of the 14th International Conference on Enterprise Information Systems - Volume 2: ICEIS, ISBN 978-989-8565-11-2, pages 105-112. DOI: 10.5220/0004003801050112

in Bibtex Style

@conference{iceis12,
author={Manuel I. Capel and Luis E. Mendoza Morales},
title={A Formal Compositional Verification Approach for Safety–Critical Systems Correctness - Model–Checking based Methodological Approach to Automatically Verify Safety Critical Systems Software},
booktitle={Proceedings of the 14th International Conference on Enterprise Information Systems - Volume 2: ICEIS,},
year={2012},
pages={105-112},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0004003801050112},
isbn={978-989-8565-11-2},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 14th International Conference on Enterprise Information Systems - Volume 2: ICEIS,
TI - A Formal Compositional Verification Approach for Safety–Critical Systems Correctness - Model–Checking based Methodological Approach to Automatically Verify Safety Critical Systems Software
SN - 978-989-8565-11-2
AU - I. Capel M.
AU - E. Mendoza Morales L.
PY - 2012
SP - 105
EP - 112
DO - 10.5220/0004003801050112