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

 

Author: 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

 

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

 

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: http://dx.doi.org/10.1504/IJCCBS.2014.059593

 

Available online 02 Mar 2014

 

 

Editors Full Text AccessAccess for SubscribersPurchase this articleComment on this article