↓Skip to main content

Real-Time Specification Patterns and Tools

Verification Time Petri Nets Patterns
Table of Contents

Nouha Abid, Silvano Dal Zilio, Didier Le Botlan
In FMICS 2012 — 17th International Workshop on Formal Methods for Industrial Critical Systems, sep 2012.

conference paper

 PDF  DOI〈10.1007/978-3-642-32469-7_1〉

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.

References
#

  • An extended version of this paper appears as Research Report LAAS N°11364, June 2011.  PDF

Citation
#


@InProceedings{DalzilioS:fmics2012patterns,
   author    = {Abid, Nouha and {Dal Zilio}, Silvano and {Le Botlan}, Didier},
   title     = {{Real-Time Specification Patterns and Tools}},
   booktitle = {FMICS 2012 -- 17th International Workshop on Formal Methods for Industrial Critical Systems},
   series    = {Lecture Notes in Computer Science},
   volume    = {7437},
   publisher = {Springer-Verlag},
   doi = {10.1007/978-3-642-32469-7_1},
   pages     = {1--15},
   month     = sep, 
   year      = 2012
}