AN OPERATIONAL SEMANTICS AND COMPILER FOR REAL-TIME SPECIFICATIONS

The Modechart specification language is a formalism for the specificat ion and implementation of real-time systems. This paper presents the s emantics for Modechart in an operational style and a compiler for auto matically synthesizing specifications. Modechart adopts the synchronou s model of concurrency and broadcast of events, which also assumes ins tantaneous response to environment inputs. The formal syntax of Modech art is introduced first, followed by the semantics for the class of de terministic specifications, followed by the definition of the non-dete rministic semantics. The semantics introduced is shown to be equivalen t to the original semantics defined in Real-Time Logic. We argue that the operational semantics provides a more computational approach to th e semantics as well as a more intuitive, modular, yet precise, referen ce manual for the language. This semantics offers insight into the lan guage and serves as a foundation for future work based on the language . We show how the semantics (for deterministic programs) naturally der ives a Modechart compiler, which provides automatic synthesis of forma l specifications. An extension to the compiler presented provides supp ort 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 applicatio ns.