Using Indexed and Synchronous Events to Model and Validate Cyber-Physical Systems

TL;DR

This paper introduces indexed and synchronous events to enhance Timed Transition Models (TTMs) for better modeling and validation of cyber-physical systems, demonstrated through train control and nuclear shutdown case studies.

Contribution

It extends TTMs with novel indexed and synchronous events, enabling high-level specifications and improved validation of complex system requirements.

Findings

Indexed events simplify actor-specific behavior specification.

Synchronous events facilitate decomposition of simultaneous state updates.

The extended TTM tool effectively verifies safety, liveness, and real-time properties.

Abstract

Timed Transition Models (TTMs) are event-based descriptions for modelling, specifying, and verifying discrete real-time systems. An event can be spontaneous, fair, or timed with specified bounds. TTMs have a textual syntax, an operational semantics, and an automated tool supporting linear-time temporal logic. We extend TTMs and its tool with two novel modelling features for writing high-level specifications: indexed events and synchronous events. Indexed events allow for concise description of behaviour common to a set of actors. The indexing construct allows us to select a specific actor and to specify a temporal property for that actor. We use indexed events to validate the requirements of a train control system. Synchronous events allow developers to decompose simultaneous state updates into actions of separate events. To specify the intended data flow among synchronized actions, we use primed variables to reference the post-state (i.e., one resulted from taking the synchronized actions). The TTM tool automatically infers the data flow from synchronous events, and reports errors on inconsistencies due to circular data flow. We use synchronous events to validate part of the requirements of a nuclear shutdown system. In both case studies, we show how the new notation facilitates the formal validation of system requirements, and use the TTM tool to verify safety, liveness, and real-time properties.