Skip Navigation
York U: Redefine the PossibleHOME | Current Students | Faculty & Staff | Research | International
Search »FacultiesLibrariesCampus MapsYork U OrganizationDirectorySite Index
Future Students, Alumni & Visitors
2014 Technical Reports

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

Chen-Wei Wang, Jonathan S. Ostroff and Simon Hudon

Technical Report EECS-2014-03

York University

June 30 2014

Abstract

Timed Transition Models (TTMs) are event-based descriptions for modelling, specifying, and verifying discrete real-time systems. A system is composed of module instances. Each module declares an interface and a list of events. An event can be spontaneous, fair, or timed (i.e., with lower and upper time bounds). TTMs have a textual syntax, an operational semantics, and an automated tool, including an editor with type checking, a graphical simulator, and a veri er for linear-time temporal logic. In this paper, we extend TTMs and its tool with two novel modelling features: synchronous events and indexed events. Event synchronization allows developers to decompose simultaneous state updates into actions of separate events. To specify the intended data ow among synchronized actions, we reference the post-state (i.e., one resulted from taking the synchronized actions) using primed variables. The TTM tool automatically infers the data ow from synchronous events, and reports type errors when there are inconsistencies due to circular data ow. We apply synchronous events to verify function blocks from the IEC 61131 standard, and a part of the requirements of a nuclear shutdown system. Indexed events allow for concise description of behaviour common to a (possibly unspecified) set of actors. The indexing construct allows us to select a specific actor and specify a temporal property for that actor. We use indexed events to verify a mutual exclusion protocol and a train system. In all examples, the TTM tool is used to verify safety, liveness, and real-time properties.

Download paper in PDF format.



The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.