Handling of Operating Modes in Contract-Based Timing Specifications

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