@inproceedings{86edfb6123c54176899e4dc9379a0673,
title = "Formal verification of user-level real-time property patterns",
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.",
keywords = "Time Petri net, model checking, observer, property pattern, real-time requirements",
author = "Ning Ge and Marc Pantel and \{Dal Zilio\}, Silvano",
note = "Publisher Copyright: {\textcopyright} 2017 IEEE.; 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017 ; Conference date: 13-09-2017 Through 15-09-2017",
year = "2017",
month = jul,
day = "2",
doi = "10.1109/TASE.2017.8285630",
language = "英语",
series = "Proceedings - 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "1--8",
booktitle = "Proceedings - 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017",
address = "美国",
}