↓Skip to main content

Formal Verification of User-Level Real-Time Property Patterns

Verification Time Petri Nets Patterns
Table of Contents

Ning Ge, Marc Pantel, Silvano Dal Zilio
In TASE 2017 — 11th International Symposium on Theoretical Aspects of Software Engineering, sep 2017.

conference paper

 PDF  DOI〈10.1109/TASE.2017.8285630〉  HAL-01589479

Abstract
#

To ease the expression of real-time requirements, Dwyer, and then Konrad, studied a large collection of existing systems in order to identify a set of real-time property patterns covering most of the useful use cases. The goal was to provide a set of reusable patterns that system designers can instantiate to express requirements instead of using complex temporal logic formulas. A limitation of this approach is that the choice of patterns is more oriented towards expressiveness than efficiency; meaning that it does not take into account the computational complexity of checking patterns. For this purpose, we define a set of verification-dedicated, atomic property patterns for qualitative and quantitative real-time requirements. End-user requirements can then be expressed as a composition of these patterns using a predefined meta-model and a mapping library. These properties can be checked efficiently using a set of elementary observers and a model checking approach.

Citation
#


@InProceedings{DalzilioS:tase2017patterns,
   author    = {Ge, Ning and Pantel, Marc and {Dal Zilio}, Silvano},
   title     = {{Formal Verification of User-Level Real-Time Property Patterns}},
   booktitle = {TASE 2017 -- 11th International Symposium on Theoretical Aspects of Software Engineering},
   publisher = {IEEE Computer Society},
   doi = {10.1109/TASE.2017.8285630},
   month     = sep, 
   year      = 2017
}