Handling of Operating Modes in Contract-based Timing Specifications

BIB
Janis Kröger and Björn Koopmann and Ingo Stierand and Nadra Tabassam and Martin Fränzle
Proceedings of the 15th International Verification and Evaluation of Computer and Communication Systems (VECoS'21)
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.
11 / 2021
To appear
inproceedings
Springer
Lecture Notes in Computer Science
Step-Up!CPS
Software-Methoden und Technologien für Modulare Updates von Cyber-Physischen Systemen
PANORAMA
Boosting Design Efficiency for Heterogeneous³ Systems

OFFIS Autoren

Martin Fränzle
Martin Fränzle