This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Compositional Semantics of a Real-Time Prototyping Language
May 1993 (vol. 19 no. 5)
pp. 453-477

The formal semantics of a prototyping language for hard real-time systems, PSDL, is given. PSDL provides a data flow notation augmented by application-orientation timing and control constraints to describe a system as a hierarchy of networks of processing units communicating via data streams. The semantics of PSDL are defined in terms of algebraic high-level Petri nets. This formalism combines algebraic specifications of abstract data types with process and concurrency concepts of Petri nets. Its data abstraction facilities are used to define the meaning of PSDL data types, while high-level Petri nets serve to model the casual and timing behavior of a system. The net model exposes potential concurrency of computation and makes all synchronization needs implied by timing and control constraints explicit and precise. Time is treated as state of clocks, and clocks are modeled as ordinary system components. The net semantics provides the basis for applying analysis techniques and semantic tools available for high-level Petri nets.

[1] R.J. Lauber, "Forecasting real-time behavior during software design using a case environment,"Real-Time Syst., vol. 1, June 1989.
[2] Luqi, V. Berzins, and R. Yeh, "A prototyping language for real-time software,"IEEE Trans. Software Eng., pp. 1409-1423, Oct. 1988.
[3] V. Berzins and Luqi, "Semantics of a real-time language," inProc. Real-Time Syst. Symp., Huntsville, AL, Dec. 1988, pp. 106-110, Computer Society Press.
[4] F. De Cindio, G. De Michelis, L. Pomello, and C. Simone, "Real system modeling: A formal but realistic approach to organizational design," in H. Wedde, Ed.,Adequate Modeling of Systems. Berlin, Heidelberg, New York: Springer-Verlag, 1983, pp. 134-152.
[5] G. Richter, "Clocks and their use for time modeling," inInformation Systems: Theoretical and Formal Aspects, A. Sernadas, J. Bubenko, Jr., and A. Olivé, Eds. Amsterdam: North-Holland, 1985, pp. 49-66. (Also published in [16], pp. 239-256.)
[6] C. A. Petri, "Forgotten topics of net theory," in W. Brauer, W. Reisig, and G. Rozenberg, Eds., Petri Nets: Applications and Relationships to Other Models of Concurrency, no. 255 inLecture Notes in Computer Science. Berlin, Heidelberg, New York: Springer-Verlag, 1987, pp. 500-514.
[7] Luqi and M. Ketabbchi, "A computer aided prototyping system,"IEEE Software, pp. 66-72, Mar. 1988.
[8] B. Krämer and H.W. Schmidt, "Architecture and functionality of a specification environment for distributed systems," in G. Knafl, Ed.,Proc. COMPSAC'90, Computer Society Press, 1990, pp. 617-622.
[9] F. Feldbrugge and K. Jensen, "Computer tools for high-level Petri nets," in K. Jensen and G. Rozenberg, Eds.,High-Level Petri Nets: Theory and Application. Berlin, Heidelberg, New York: Springer-Verlag, 1991, pp. 691-717.
[10] Proc. 1st Int. Workshop Timed Petri Nets, Torino, Italy, 1985, Computer Society Press.
[11] Proc. Int. Workshop Petri Nets and Performance Models, Madison, Wl, 1987, Computer Society Press.
[12] C. Ghezzi, D. Mandrioli, S. Morasca and M. Pezzè, "A general way to put time in Petri nets," inProc. 5th Int. Workshop Software Specifications and Design, Pittsburgh, PA, May 19-20, 1989. Washington, DC: IEEE Computer Society Press, 1989.
[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] G.H. MacEwen and D.B. Skillicorn, "Using higher-order logic for modular specification of real-time distributed systems, in M. Joseph, Ed.,Formal Techniques in Real-Time and Fault-Tolerant Systems, no. 331 in Lecture Notes in Computer Science, 10 Berlin, Heidelberg, New York: Springer-Verlag, 1988, 36-66.
[15] G.M. Reed and A.W. Roscoe, "A timed model for communicating sequential processes,"J. Theoret. Comput. Sci., vol. 58, pp. 249-261,1988.
[16] T.A. Henzinger, Z. Manna, and A. Pnueli, "An interleaving model for real-time," Tech. Rep. STAN-CS-1329, Stanford, Univ., Palo Alto, CA, Sept. 1990.
[17] A. Pnueli and E. Harel, "Applications of temporal logic to the specification of real-time systems," inProc. Formal Techniques in Real-Time and Fault-Tolerant Systems (LNCS 331), pp. 84-98, 1988.
[18] P.H. Starke, "Remarks on timed nets," inProc. 9th European Workshop Appl. and Theory of Petri Nets, 1988, pp. 216-228.
[19] C. Ghezzi, D. Mandrioli, S. Morasca, and M. Pezzè, "A unified high-level Petri net formalism for time-critical systems,"IEEE Trans. Software Eng., vol. 17, pp. 160-172, 1991.
[20] B. Auernheimer and R. A. Kemmerer, "RT-ASLAN: A specification language for real time systems,"IEEE Trans. Software Eng., vol. SE-12, pp. 879-889, Sept. 1986.
[21] M.R. Barbacci and J.M. Wing, "Specifying functional and timing behavior for real-time applications," in J.W. de Bakker, A.J. Nijman, and P.C. Treleaven, Eds.,PARLE Parallel Architectures and Languages Europe, no. 259 in Lecture Notes in Computer Science, Berlin, Heidelberg, New York: Springer-Verlag, 1987, pp. 124-140.
[22] J.V. Guttag, J.J. Horning, and J.M. Wing, "The Larch family of specification languages,"IEEE Software, pp. 24-36, Sept. 1985.
[23] V. Berzins and Luqi,Software Engineering with Abstractions: An Integratd Approach to Software Development Using Ada, Addison-Wesley, Reading, Mass., 1990.
[24] B. Krämer, Luqi, and V. Berzins, "Denotational semantics of a real-time prototyping language," Tech. Rep. NPS 52-90-33, Dept. Comput. Sci., Naval Postgraduate School, 1990.
[25] Luqi, "Knowledge-based support for rapid prototyping,"IEEE Expert, 9-18, Winter 1988.
[26] B. Krämer and H.W. Schmidt, "A high level net language for modeling organisational systems," in H. Wedde, Ed.,Adequate Modeling of Systems. Berlin, Heidelberg, New York: Springer-Verlag, 1982, pp. 156-170.
[27] H.J. Genrich and K. Lautenbach, "Systems modelling with high-level Petri nets,"J. Theoret. Comput. Sci., vol. 13, no. 1, pp. 109-136, 1981.
[28] S. Raudys, "On the accuracy of a bootstrap estimate of the classification error," inProc. 9th Int. Conf. Pattern Recognition, Rome, Italy, Nov. 1988, p. 1230-1232.
[29] B. Krämer and H.W. Schmidt, "Types and modules for net specifications," in K. Voss, H.J. Genrich, and G. Rozenberg, Eds.,Concurrency and Nets. Berlin, Heidelberg, New York: Springer-Verlag, 1987, pp. 269-286.
[30] B. Krämer,Concepts, Syntax and Semantics of SEGRAS--A Specification Language for Distributed Systems. München, Wien: Oldenbourg Verlag, 1989.
[31] B. Berthomieu, N. Choquet, C. Colin, B. Loyer, J.M. Martin, and A. Mauboussin, "Abstract data nets combining Petri nets and abstract data types for high level specifications of distributed systems," inProc. 7th European Workshop Appl. and Theory of Petri Nets, Oxford, England, July 1986, pp. 25-48.
[32] E. Battiston, F. De Cindio, and G. Mauri, "OBJSA nets: A class of high-level nets having objects as domains," in G. Rozenberg, Ed.,Advances in Petri Nets 1988, no. 340 inLecture Notes in Computer Science. Berlin, Heidelberg, New York: Springer-Verlag, 1988, pp. 20-43.
[33] W. Reisig, "Petri nets and algebraic specifications,"J. Theoret. Comput. Sci., vol. 80, pp. 1-34, 1991.
[34] J. Vautherin, "Parallel systems specifications with coloured Petri nets and algebraic abstract data types," in G. Rozenberg, Ed.,Advances in Petri Nets 1987, no. 266 inLecture Notes in Computer Science. Berlin, Heidelberg, New York: Springer-Verlag, 1987, pp. 293-308.
[35] J. Billington, "Many-sorted high-level nets," inProc. 3rd Int. Workshop Petri Nets and Performance Models, Kyoto, Japan, 1989, pp. 166-179, Computer Society Press.
[36] C. Dimitrovici, U. Hummert, and L. Petrucci, "Semantics, composition and net properties of algebraic high-level nets," in G. Rozenberg, Ed.,Advances in Petri Nets 1991, no. 524 inLecture Notes in Computer Science. Berlin, Heidelberg, New York: Springer-Verlag, 1991, pp. 93-117.
[37] K. Jensen, "coloured Petri nets and the invariant-method,"J. Theoret. Comput. Sci., vol. 14, pp. 317-336, 1981.
[38] K. Jensen and G. Rozenberg, Eds.High-Level Petri Nets; Theory and Application. New York: Springer-Verlag, 1991.
[39] J. A. Goguen, J.W. Thatcher, and E.G. Wagner, "An initial algebra approach to the specification, correctness, and implementation of abstract data types," in R. Yeh, Ed.,Current Trends in Programming Methodology, Volume IV, Data Structuring, Englewood Cliffs, NJ: Prentice-Hall, 1978, pp. 80-149.

Index Terms:
compositional semantics; real-time prototyping language; formal semantics; hard real-time systems; PSDL; data flow notation; application-orientation timing; control constraints; algebraic high-level Petri nets; algebraic specifications; abstract data types; concurrency concepts; timing behavior; synchronization; abstract data types; formal specification; Petri nets; real-time systems; software prototyping; specification languages
Citation:
B. Kramer, Luqi, V. Berzins, "Compositional Semantics of a Real-Time Prototyping Language," IEEE Transactions on Software Engineering, vol. 19, no. 5, pp. 453-477, May 1993, doi:10.1109/32.232012
Usage of this product signifies your acceptance of the Terms of Use.