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

National audienceAn 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