Regresar

Compositional model-checking verification of critical systems

Abstract:

Ensuring the correctness of Critical Systems (CS) becomes more complex if we consider that their behaviour is the result of the concurrent execution of many components. Furthermore, any automaton-based representation of concurrent components yields an explosion in the number of states, thus limiting the use of Model-Checking (MC) verification techniques in practice. This article presents a compositional verification approach, which is formally supported by state-of-the-art MC tools. To facilitate and guarantee the verification of large CS, the proposed approach integrates MEDISTAM-RT (Spanish acronym of Method for System Design based on Analytic Transformation of Real-Time Models), CCTL temporal logic as the property specification formal language, and the formal language CSP+T, used to formally describe a model of the system to be verified. To show a practical use of the proposed approach, a critical part of a realistic industry project related to mobile phone communications is discussed. © 2009 Springer Berlin Heidelberg.