This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Communicating Real-Time State Machines
September 1992 (vol. 18 no. 9)
pp. 805-816

Communicating real-time state machines (CRSMs), a complete and executable notation for specifying concurrent real-time systems including the monitored and controlled physical environment, are introduced. They are essentially state machines that communicate synchronously in a manner much like the input-output in Hoare's CSP. In addition, CRSMs have a novel and small set of facilities for describing timing properties and accessing real time. The author defines the CRSM language, gives many examples of its use in requirements specification, outlines an algorithm for executing or simulating CRSMs, introduces some techniques for reasoning about the specifications, and discusses some open problems and issues.

[1] G. S. Avrunin, L. K. Dillon, J. C. Wileden, and W. E. Riddle, "Constrained expressions: adding analysis capabilities to design methods for concurrent software systems,"IEEE Trans. Software Eng., vol. SE- 12, pp. 278-292, Feb. 1986.
[2] S. Bearet al., "Graphical specification of object-oriented systems,"Proc. ECCOP/OOPSLA 90, SIGPLAN Notices 25, pp. 28-37, Oct. 1990.
[3] L. Cardelli and R. Pike, "Squeak: A language for communicating with mice,"Proc SIGGRAPH 85, ACM SIGGRAPH 19, pp. 199-204, July 1985.
[4] J. Davies and S. Schneider, "An introduction to timed CSP,"Tech. Monograph PRG-75, Oxford University Computing Laboratory, Aug. 1989.
[5] A. Gabrielian and M. Franklin,"Multilevel specification of real-time systems,"Comm. of ACM 34, pp. 51-60, May 1991.
[6] R. Gerber and I. Lee, "Communicating shared resources: A model for distributed real-time systems,"Proc. IEEE Real-Time Systems Symp., pp. 68-78, Dec. 1989.
[7] G. Ghezzi, D. Mandrioli, S. Morasea, and M. Pezzè, "A unified high-level Petri net formalism for time-critical systems,"IEEE Trans. Software Eng. 17, vol. 2, pp. 160-172, Feb. 1991.
[8] D. Harel, "Statecharts: A visual formalism for complex systems,"Sci. Comput. Program., vol. 8, pp. 231-274, 1987.
[9] C. A. R. Hoare, "An axiomatic basis for computer programming,"Commun. ACM, vol. 12, no. 10, pp. 576-583, 1969.
[10] C. A. R. Hoare, "Communicating sequential processes,"Commun. ACM, vol. 21, pp. 666-677, 1978.
[11] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[12] M. Jaffe, N. Leveson, M. Heimdahl, and B. Melhart, "Software requirements analysis for real-time process control systems,"IEEE Trans. Software Eng., vol. 17, pp. 241-258, Mar. 1991.
[13] 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.
[14] S. Jahanian and A. Mok, "Modechart: A Specification Language Real Time Systems",IEEE Trans. on Software Eng.(to appear). IBM Tech Report RC 15140, Nov. 1989.
[15] H. Jarvinen, R. Kurki-Suonio, M. Sakkinen, and K. Systa, "Object-oriented specification of reactive systems," inProc. 12th IEEE Conf. Software Eng., pp. 63-71, 1990.
[16] N.G. Leveson and J.L. Stolzy, "Safety analysis using Petri nets,"IEEE Trans. Software Eng., vol. SE-13, no. 3, pp. 386-397, Mar. 1987.
[17] N. Lynch and M. Tuttle, "An introduction to input/output automata,"CWI - Quarterly 2, 1989; also,Tech. Memo. MIT/LCS/TM-373, Laboratory for Computer Science, MIT, Nov. 1988.
[18] J. Ostroff and W. Wonham, "Modeling and verifying real-time embedded computer systems," inProc. IEEE Real-Time Systems Symp., pp. 124-132, Dec. 1987.
[19] S. Raju, "Formal object-oriented specifications for real time systems," Internal Working Paper, Dept. Computer Science and Engineering, Univ. Washington, June 1991.
[20] G. Reed and A. Roscoe, "A timed model for communicating sequential processes, " inProc. ICALP '86, Springer-Verlag LCNS 226, 1986, pp. 314-323.
[21] A. Shaw, "Software descriptions with flow expressions,"IEEE Trans. Software Eng., vol. SE-4, pp. 242-254, May 1978.
[22] A. Shaw, "Reasoning about time in higher-level language software,"IEEE Trans. Software Eng., vol. 15, pp. 875-889, July 1989.
[23] A. Shaw, "Deterministic Timing Schema for Parallel Programs," Tech. Report 90-05-06, Dept. of Computer Science and Engineering, Univ. of Washington, Seattle, May, 1990. (To appear inProc. Fifth Int'l Parallel Processing Symp., CS Press, Order No. 2167, Los Alamitos, Calif., Apr. 1991.)

Index Terms:
communicating real-time state machines; executable notation; concurrent real-time systems; controlled physical environment; state machines; CRSMs; timing properties; CRSM language; requirements specification; communicating sequential processes; finite state machines; formal specification; parallel machines; real-time systems
Citation:
A.C. Shaw, "Communicating Real-Time State Machines," IEEE Transactions on Software Engineering, vol. 18, no. 9, pp. 805-816, Sept. 1992, doi:10.1109/32.159840
Usage of this product signifies your acceptance of the Terms of Use.