This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Stepwise Design of Real-Time Systems
January 1993 (vol. 19 no. 1)
pp. 56-69

The joint action approach to modeling of reactive systems is presented and augmented with real time. This leads to a stepwise design method where temporal logic of actions can be used for formal reasoning, superposition is the key mechanism for transformations, the advantages of closed-system modularity are utilized, logical properties are addressed before real-time properties, and real-time properties are enforced without any specific assumptions on scheduling. As a result, real-time modeling is made possible already at early stages of specification, and increased insensitivity is achieved with respect to properties imposed by implementation environments.

[1] J.-R. Abrial, "Programming as a mathematical exercise," inMathematical Logic and Programming Languages, C. A. R. Hoare and J. C. Shepherdson, Eds. Englewood Cliffs, NJ: Prentice-Hall, 1985.
[2] B. Alpern and F. B. Schneider, "Defining liveness,"Inform. Processing Lett., vol. 21, no. 4, pp. 181-185, Oct. 1985.
[3] R. J. R. Back and R. Kurki-Suonio, "Decentralization of process nets with a centralized control,"Distributed Computing, vol. 3, pp. 73-87, 1989. An earlier version appears inProc. 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, pp. 131-142, 1983.
[4] R. J. R. Back and R. Kurki-Suonio, "Serializability in distributed systems with handshaking," inAutomata, Languages and Programming, T. Lepisto and A. Salomaa, Eds. New York: Springer-Verlag, 1988, pp. 52-66.
[5] R. J. R. Back and R. Kurki-Suonio, "Distributed cooperation with Action Systems,"ACM Trans. Programming Languages Syst., vol. 10, no. 4, pp. 513-554, Oct. 1988.
[6] T. Bolognesi and E. Brinksma, "Introduction to the ISO Specification language LOTOS,"Computer Networks ISDN Syst., vol. 14, pp. 25- 59, 1987.
[7] K. M. Chandy and J. Misra,Parallel Program Design: A Foundation. Reading, MA: Addison-Wesley, 1988.
[8] E. W. Dijkstra and C. S. Scholten, "Termination detection for diffusing computations,"Inform. Processing Lett., vol. 11, no. 1, pp. 1-4, Aug. 1980.
[9] M. Evangelist, N. Francez, and S. Katz, "Multiparty interactions for interprocess communication and synchronization,"IEEE Trans. Software Eng., vol. 15, no. 11, pp. 1417-1426, Nov. 1989.
[10] N. Francez and I. R. Forman, "Interacting processes: A language coordinated distributed programming," inProc. 5th Jerusalem Conf. Inform. Technol., IFIP (also available as Tech. Rep. STP-226-90, MCC, 1990).
[11] J. Hooman and J. Widom, "A temporal-logic based compositional proof system for real-time message passing, inPARLE'89 Parallel Architectures and Languages Europe, vol. II, E. Odijk, M. Rem, and J.-C. Syr, Eds. New York: Springer-Verlag, 1989, pp. 424-441.
[12] J. D. Ichbiahet al., "Rationale for the design of the Ada programming language,"SIGPLAN Notices, vol. 14, (Tech. Rep. 6), pt. B, June 1979.
[13] H.-M. Järvinen, "The design of a specification language for reactive systems," Ph.D. dissertation, Tampere University of Technology, publ. 95, 1992.
[14] H.-M. Järvinen and R. Kurki-Suonio, "DisCo specification language: Marriage of actions and objects," inProc. 11th Int. Conf. on Distributed Computing Syst., 1991, pp. 142-151.
[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] C.B. Jones,Systematic Software Development Using VDM, Prentice Hall Int'l, 1986.
[17] R. Kurki-Suonio, "Toward programming with knowledge expressions," inProc. 13th Annu. ACM Symp. on Principles of Programming Languages, 1986, pp. 140-149.
[18] R. Kurki-Suonio, "Stepwise design of real-time systems," inProc. ACM SIGSOFT Conf. on Software for Critical Systems, Software Engineering Notes, vol. 16, no. 5, Dec. 1991, pp. 120-131.
[19] R. Kurki-Suonio, "Operational specification with joint actions: Serializable databases,"Distributed Computing, vol. 6, no. 1, pp. 19-37, 1992.
[20] R. Kurki-Suonio, "Modular modeling of temporal behaviors," inInformation Modeling and Knowledge Bases III, S. Ohsuga, H. Kangassalo, H. Jaakkola, K. Hori, and N. Yonezaki, Eds. Amsterdam: IOS Press, 1992, pp. 283-300.
[21] R. Kurki-Suonio and H.-M. Järvinen, "Action system approach to the specification and design of distributed systems," inProc. 5th International Workshop on Software Specification and Design, ACM Software Engineering Notes, vol. 14, no. 3, pp. 34-40, May 1989.
[22] R. Kurki-Suonio, K. Systä, and J. Vain, "Real-time specification and modeling with joint actions," to appear inSci. Computer Programming. An earlier version appeared inProc. 6th Int. Workshop on Software Specification and Design, 1991, pp. 84-91.
[23] L. Lamport, "The temporal logic of actions," Tech. Rep. 79, Digital Equipment Corp., Systems Research Center, 1991.
[24] L. Lamport, personal communication, 1991.
[25] H. W. Lawson, "Philosophies for engineering computer-based systems,"Computer, vol. 23, no. 12, pp. 52-63, Dec. 1990.
[26] H. W. Lawson, "Cy-Clone--An approach to the engineering of resource adequate cyclic real-time systems,"Real-Time Syst., vol. 4, no. 1, pp. 55-83, Mar. 1992.
[27] L. Y. Liu and R.K. Shyamasundar, "Static analysis of real-time distributed systems,"IEEE Trans. Software Eng., vol. 16, no. 4, pp. 373-388, Apr. 1990.
[28] Z. Manna and A. Pnueli, "How to cook a temporal proof system for your pet language," inProc. Symp. Principles Programm. Languag., Austin, TX, Jan. 1983, pp. 141-154.
[29] A. Pnueli, "Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of CurrentTrends," inCurrent Trends in Concurrency: Overviews and Tutorials. W.-P. de Roever and G. Rozenberg, eds., Lecture Notes in Computer Science 224, Springer-Verlag, N.Y., 1986, pp. 510-584.
[30] W.-P. de Roever, "Foundations of computer science: Leaving the ivory tower,"EATCS Bull., no. 44, pp. 455-492, June 1991.
[31] A. Salwicki and T. Muldner,On the Algorithmic Properties of Concurrent Programs. New York: Springer-Verlag, 1981.
[32] K. Systä, "A graphical tool for specification of reactive systems," inProc. Euromicro '91 Workshop on Real-Time Systems, 1991, pp. 12-19.
[33] K. Systäand R. Kurki-Suonio, "Modeling of distributed real-time systems in Disco," inProc. 4th Euromicro Workshop on Real-Time Systems, 1992, pp. 136-141.
[34] P. Ward and S. Mellor,Structured Development for Real-Time Systems, Vols. 1-3, Yourdon Press, New York, 1985.
[35] N. Wirth, "Toward a discipline of real-time programming,"Commun. ACM, vol. 20, no. 8, Aug. 1977.

Index Terms:
real-time systems; reactive systems; stepwise design method; temporal logic; formal reasoning; closed-system modularity; real-time properties; scheduling; formal specification; real-time systems; temporal logic
Citation:
R. Kurki-Suonio, "Stepwise Design of Real-Time Systems," IEEE Transactions on Software Engineering, vol. 19, no. 1, pp. 56-69, Jan. 1993, doi:10.1109/32.210307
Usage of this product signifies your acceptance of the Terms of Use.