Abstract We describe a toolset, consisting of a graphical editor, a simulator, and an assertion checker, for prototyping real‐time systems that are specified as Communicating Real‐Time State machines (CRSMs). CRSMs are timed state machines that communicate synchronously over unidirectional channels. The system behavior of CRSMs is characterized by a time‐stamped trace of communication events. Safety and timing assertions on the trace of communication events are expressed in a notation based on Real‐Time Logic. We illustrate the simulator and assertion checker by specifying a traffic‐light controller and other real‐time systems. There are two main contributions in this work: first, the prototyping environment serves as a validation of the model, the execution algorithm and paper design of example CRSMs, demonstrating that the ideas are realizable and potentially useful. Secondly, the paper presents a novel and useful method of specifying safety and timing properties, and checking them during simulation.

A run-time environment for monitoring distributed real-time systems is described. In particular, the authors focus on the problem of detecting violations of timing assertions in an environment in which the real-time tasks run on multiple processors, and timing constraints can be either interprocessor or intraprocessor constraints. Constraint violations are detected at the earliest possible time by deriving and checking intermediate constraints. If the violations must be detected as early as possible, then the problem of minimizing the number of messages to be exchanged between the processors becomes intractable. The authors characterize a subclass of timing constraints that occur commonly in distributed real-time systems and whose message requirements can be minimized. They also take into account the drift among the various processor clocks when detecting a violation of a timing assertion. Finally, an implementation of a distributed run-time monitor is described.>