@inproceedings{Jan2021,
Author = {Janis Kröger and Björn Koopmann and Ingo Stierand and Nadra Tabassam and Martin Fränzle},
Title = {Handling of Operating Modes in Contract-based Timing Specifications},

Year = {2021},
Month = {11},
Publisher = {Springer},
Series = {Lecture Notes in Computer Science},
Isbn = {To appear},
Booktitle = {Proceedings of the 15th International Verification and Evaluation of Computer and Communication Systems (VECoS'21)},
type = {inproceedings},
Abstract = {The design of safety-critical systems calls for rigorous application of specification and verification methods. In this context, a comprehensive consideration of safety aspects, which inevitably include timing properties, requires explicit addressing of operating modes and their transitions in the system model as well as in the respective specifications. As a side effect, this helps to reduce verification complexity.

This paper presents an extension of a framework for the specification of timing properties following the contract-based design paradigm. It provides enhancements of the underlying specification language that enable specifying mode-dependent behavior as well as how mode transitions may take place. A formal specification is given in order to enable reasoning about such specifications as well as contract operations like refinement and composition, thus enabling to make statements about mode composition. The results are discussed using a real-world example.}
}
@COMMENT{Bibtex file generated on }