A Verified Approach to Checking Real-Time Patterns on Fiacre Programs

Nouha Abid (1) , Silvano Dal Zilio (1)

1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques

An issue limiting the adoption of model-checking technologies by the industry is the ability, for non-experts, to express their requirements using the property languages supported by verification tools. This has motivated the definition of dedicated assertion languages for expressing temporal properties at a higher level. However, only a limited number of these formalisms support the definition of timing constraints and even fewer of them take into account the complexity of checking properties on a system. In this paper, we propose a complete framework that includes: the definition of timed patterns; a tool chain for checking timed properties; and methods to prove the correctness of our verification approach.

Domaines: Systèmes embarqués; Logique en informatique [cs.LO]

Nouha Abid, Silvano Dal Zilio. A Verified Approach to Checking Real-Time Patterns on Fiacre Programs. Doctoral Symposium of FM 2012, Aug 2012, Paris, France. ⟨hal-01790120⟩