Title: A formal framework to specify and verify real-time properties on critical systems

Authors: Nouha Abid; Silvano Dal Zilio; Didier Le Botlan

Addresses: CNRS, LAAS, 7 Avenue du Colonel Roche, F-31400 Toulouse, France; Univ Toulouse, LAAS, F-31400 Toulouse, France; Univ Toulouse, INSA, LAAS, F-31400 Toulouse, France ' CNRS, LAAS, 7 Avenue du Colonel Roche, F-31400 Toulouse, France; Univ Toulouse, LAAS, F-31400 Toulouse, France; Univ Toulouse, INSA, LAAS, F-31400 Toulouse, France ' CNRS, LAAS, 7 Avenue du Colonel Roche, F-31400 Toulouse, France; Univ Toulouse, LAAS, F-31400 Toulouse, France; Univ Toulouse, INSA, LAAS, F-31400 Toulouse, France

Abstract: We propose a verified approach to the formal verification of timed properties using model-checking techniques. We focus on properties commonly found during the analysis of reactive systems, expressed using real-time specification patterns. We use observers in order to transform the verification of these timed patterns into the verification of simpler LTL formulas. While the use of observers for model-checking is quite common, our contribution is original in several ways. First, we define a formal framework to verify that observers are correct and non-intrusive. Second, we define different classes of observers for each pattern and use a pragmatic approach in order to select the most efficient candidate in practice. This approach is implemented in an integrated verification tool chain for the Fiacre language.

Keywords: formal verification; requirements specification; patterns; model checking; time Petri nets; TPNs; Fiacre; timed properties.

DOI: 10.1504/IJCCBS.2014.059593

International Journal of Critical Computer-Based Systems, 2014 Vol.5 No.1/2, pp.4 - 30

Published online: 21 Oct 2014 *

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