An Operational Semantics and Compiler for Real-Time Specifications

The Modechart specification language is a formalism for the specification and implementation of real-time systems. The semantics of the language was formally defined axiomatically in Real-Time Logic. This paper presents the semantics for Modechart in an operational style and a compiler for automatically synthesizing specifications. Modechart is a synchronous language, which assumes the synchronous model of concurrency and broadcast of events. The synchronous model assumes the system to be theoretically much faster than the environment. Modechart allows both deterministic and non-deterministic real-time specifications. The semantics for the class of deterministic specifications is introduced first, followed by the definition of the nondeterministic semantics. The deterministic semantics naturally derives a Modechart compiler, which provides automatic synthesis of formal specifications. An extension to the compiler presented provides support for a subset of the class of non-deterministic..