This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Modechart: A Specification Language for Real-Time Systems
December 1994 (vol. 20 no. 12)
pp. 933-947

Present a specification language for real-time systems called Modechart. The semantics of Modechart is given in terms of real-time logic (RTL), which 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 results 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 are given. A graphical implementation of Modechart has been completed.

[1] M. W. Alford, "A requirements engineering methodology for real-time processing requirements,"IEEE Trans. Software Eng., vol. SE-3, Jan. 1977.
[2] C. G. Davis and C. R. Vick, "The software development system,"IEEE Trans. Software Eng., vol. SE-3, pp. 69-84, Jan. 1977.
[3] D. Harel, "Statecharts: A visual formalism for complex systems," The Weizmann Inst. of Sci., Israel, Tech. Rep., July 1986.
[4] D. Harel, A. Pnueli, J. P. Schmidt, and R. Sherman, "On the formal semantics of statecharts," inProc. 2nd Symp. Logic in Comput. Sci., June 1987, pp. 54-64.
[5] K. L. Heninger, "Specifying software requirements for complex systems: New techniques and their application,"IEEE Trans. Software Eng., vol. SE-6, pp. 2-13, Jan. 1980.
[6] F. Jahanian, R. S. Lee, and A. K. Mok, "Semantics of Modechart in real-time logic," inProc. 21st Hawaii Int. Conf. Syst. Sci., Jan. 1988.
[7] F. Jahanian, A. K. Mok, and D. A. Stuart, "Formal specification of real-time systems," Dep. of Comput. Sci., Univ. of Texas at Austin, Tech. Rep. TR-88-25, June 1988.
[8] F. Jahanian and A. K. Mok, "Safety analysis of timing properties in real-time systems,"IEEE Trans. Software Eng., vol. SE-12, no. 9, pp. 890-904, Sept. 1986.
[9] Luqi and V. Berzins, "Rapid prototyping of real-time systems,"IEEE Software, Sept. 1988.
[10] A. K. Mok, "SARTOR--A design environment for real-time systems," inProc. 9th IEEE COMPSAC, Chicago, IL, Oct. 1985, pp. 174-181.
[11] A. Pnueli, private communication, 1987.
[12] D. Parnas, K. L. Heninger, J. W. Kallander, and J. E. Shore, "Software requirements for the A-7E aircraft," NRL memo. rep. 3876, Washington, DC, Nov. 1978.
[13] P. Zave, "A distributed alternative to finite-state-machine specifications,"ACM Trans. Programming Languages and Syst., vol. 7, no. 1, pp. 10-36, Jan. 1985.

Index Terms:
real-time systems; specification languages; logic programming languages; Modechart; specification language; real-time systems; semantics; real-time logic; absolute timing; real-time clock; RTL formulas; hierarchical organization; RTL assertions; abstraction levels; graphical implementation; rapid prototyping; timing constraints; SARTOR
Citation:
F. Jahanian, A.K. Mok, "Modechart: A Specification Language for Real-Time Systems," IEEE Transactions on Software Engineering, vol. 20, no. 12, pp. 933-947, Dec. 1994, doi:10.1109/32.368134
Usage of this product signifies your acceptance of the Terms of Use.