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. This paper presents the semantics for Modechart in an operational style and a compiler for automatically synthesizing specifications. Modechart adopts the synchronous model of concurrency and broadcast of events, which also assumes instantaneous response to environment inputs. The formal syntax of Modechart is introduced first, followed by the semantics for the class of deterministic specifications, followed by the definition of the non-deterministic semantics. The semantics introduced is shown to be equivalent to the original semantics defined in Real-Time Logic. We argue that the operational semantics provides a more computational approach to the semantics as well as a more intuitive, modular, yet precise, reference manual for the language. This semantics offers insight into the language and serves as a foundation for future work based on the language. We show how the semantics (for deterministic programs) naturally derives a Modechart compiler, which provides automatic synthesis of formal specifications. An extension to the compiler presented provides support for a fragment of the non-deterministic specifications which occur often in practice. We characterize this class and show how it can be used in automatic code generation for engineering real-time applications.