Real-Time Specification Patterns and Tools
Nouha Abid (LAAS), Silvano Dal Zilio (LAAS), Didier Le Botlan (LAAS)

TL;DR
This paper introduces real-time specification patterns and an integrated tool chain for verifying timed requirements in reactive systems, addressing industry needs for accessible and expressive property languages in model checking.
Contribution
It proposes a set of real-time specification patterns and a comprehensive verification tool chain for timed properties in extended Timed Petri Nets.
Findings
Patterns effectively express real-time requirements.
The tool chain enables verification of timed properties.
Supports industry adoption of model checking for real-time systems.
Abstract
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. In this paper, we propose a set of specification patterns that can be used to express real-time requirements commonly found in the design of reactive systems. We also provide an integrated model checking tool chain for the verification of timed requirements on TTS, an extension of Timed Petri Nets with data variables and priorities.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
