MODECHART - A SPECIFICATION LANGUAGE FOR REAL-TIME SYSTEMS

In this paper, we present a specification language for real-time systems called Modechart. The semantics of Modechart is given in terms of RTL (Real Time Logic [8]) that is especially amenable to reasoning about the absolute (real-time clock) timing of events. The semantics of Modechart has an important property that the translation of a Modechart specification into RTL formulas will result in a hierarchical organization of the resulting RTL assertions. This gives us significant leverage in reasoning about properties of a system by allowing us to filter out assertions that concern lower levels of abstraction. Some results about desirable properties of Modechart specifications will be given. A graphical implementation of Modechart has been completed.