F. Jahanian et Ak. Mok, MODECHART - A SPECIFICATION LANGUAGE FOR REAL-TIME SYSTEMS, IEEE transactions on software engineering, 20(12), 1994, pp. 933-947
In this paper, we present a specification language for real-time syste
ms called Modechart. The semantics of Modechart is given in terms of R
TL (Real Time Logic [8]) that is especially amenable to reasoning abou
t the absolute (real-time clock) timing of events. The semantics of Mo
dechart has an important property that the translation of a Modechart
specification into RTL formulas will result in a hierarchical organiza
tion of the resulting RTL assertions. This gives us significant levera
ge 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.