Real-Time Specification Patterns and Tools
This addresses a domain-specific issue for industry practitioners in reactive systems, but it is incremental as it builds on existing formalisms and tools.
The paper tackles the problem of non-experts struggling to express real-time requirements for model checking by proposing a set of specification patterns and an integrated tool chain for verification on Timed Petri Nets extensions, resulting in a practical solution for reactive systems design.
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.