
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
B. Kramer, Luqi, V. Berzins, "Compositional Semantics of a RealTime Prototyping Language," IEEE Transactions on Software Engineering, vol. 19, no. 5, pp. 453477, May, 1993.  
BibTex  x  
@article{ 10.1109/32.232012, author = {B. Kramer and Luqi and V. Berzins}, title = {Compositional Semantics of a RealTime Prototyping Language}, journal ={IEEE Transactions on Software Engineering}, volume = {19}, number = {5}, issn = {00985589}, year = {1993}, pages = {453477}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.232012}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Compositional Semantics of a RealTime Prototyping Language IS  5 SN  00985589 SP453 EP477 EPD  453477 A1  B. Kramer, A1  Luqi, A1  V. Berzins, PY  1993 KW  compositional semantics; realtime prototyping language; formal semantics; hard realtime systems; PSDL; data flow notation; applicationorientation timing; control constraints; algebraic highlevel Petri nets; algebraic specifications; abstract data types; concurrency concepts; timing behavior; synchronization; abstract data types; formal specification; Petri nets; realtime systems; software prototyping; specification languages VL  19 JA  IEEE Transactions on Software Engineering ER   
The formal semantics of a prototyping language for hard realtime systems, PSDL, is given. PSDL provides a data flow notation augmented by applicationorientation 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 highlevel 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 highlevel 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 highlevel Petri nets.
[1] R.J. Lauber, "Forecasting realtime behavior during software design using a case environment,"RealTime Syst., vol. 1, June 1989.
[2] Luqi, V. Berzins, and R. Yeh, "A prototyping language for realtime software,"IEEE Trans. Software Eng., pp. 14091423, Oct. 1988.
[3] V. Berzins and Luqi, "Semantics of a realtime language," inProc. RealTime Syst. Symp., Huntsville, AL, Dec. 1988, pp. 106110, 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: SpringerVerlag, 1983, pp. 134152.
[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: NorthHolland, 1985, pp. 4966. (Also published in [16], pp. 239256.)
[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: SpringerVerlag, 1987, pp. 500514.
[7] Luqi and M. Ketabbchi, "A computer aided prototyping system,"IEEE Software, pp. 6672, 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. 617622.
[9] F. Feldbrugge and K. Jensen, "Computer tools for highlevel Petri nets," in K. Jensen and G. Rozenberg, Eds.,HighLevel Petri Nets: Theory and Application. Berlin, Heidelberg, New York: SpringerVerlag, 1991, pp. 691717.
[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 1920, 1989. Washington, DC: IEEE Computer Society Press, 1989.
[13] F. Jahanian and A. K. Mok, "Safety analysis of timing properties in realtime systems,"IEEE Trans. Software Eng., vol. SE12, no. 9, pp. 890904, Sept. 1986.
[14] G.H. MacEwen and D.B. Skillicorn, "Using higherorder logic for modular specification of realtime distributed systems, in M. Joseph, Ed.,Formal Techniques in RealTime and FaultTolerant Systems, no. 331 in Lecture Notes in Computer Science, 10 Berlin, Heidelberg, New York: SpringerVerlag, 1988, 3666.
[15] G.M. Reed and A.W. Roscoe, "A timed model for communicating sequential processes,"J. Theoret. Comput. Sci., vol. 58, pp. 249261,1988.
[16] T.A. Henzinger, Z. Manna, and A. Pnueli, "An interleaving model for realtime," Tech. Rep. STANCS1329, Stanford, Univ., Palo Alto, CA, Sept. 1990.
[17] A. Pnueli and E. Harel, "Applications of temporal logic to the specification of realtime systems," inProc. Formal Techniques in RealTime and FaultTolerant Systems (LNCS 331), pp. 8498, 1988.
[18] P.H. Starke, "Remarks on timed nets," inProc. 9th European Workshop Appl. and Theory of Petri Nets, 1988, pp. 216228.
[19] C. Ghezzi, D. Mandrioli, S. Morasca, and M. Pezzè, "A unified highlevel Petri net formalism for timecritical systems,"IEEE Trans. Software Eng., vol. 17, pp. 160172, 1991.
[20] B. Auernheimer and R. A. Kemmerer, "RTASLAN: A specification language for real time systems,"IEEE Trans. Software Eng., vol. SE12, pp. 879889, Sept. 1986.
[21] M.R. Barbacci and J.M. Wing, "Specifying functional and timing behavior for realtime 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: SpringerVerlag, 1987, pp. 124140.
[22] J.V. Guttag, J.J. Horning, and J.M. Wing, "The Larch family of specification languages,"IEEE Software, pp. 2436, Sept. 1985.
[23] V. Berzins and Luqi,Software Engineering with Abstractions: An Integratd Approach to Software Development Using Ada, AddisonWesley, Reading, Mass., 1990.
[24] B. Krämer, Luqi, and V. Berzins, "Denotational semantics of a realtime prototyping language," Tech. Rep. NPS 529033, Dept. Comput. Sci., Naval Postgraduate School, 1990.
[25] Luqi, "Knowledgebased support for rapid prototyping,"IEEE Expert, 918, 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: SpringerVerlag, 1982, pp. 156170.
[27] H.J. Genrich and K. Lautenbach, "Systems modelling with highlevel Petri nets,"J. Theoret. Comput. Sci., vol. 13, no. 1, pp. 109136, 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. 12301232.
[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: SpringerVerlag, 1987, pp. 269286.
[30] B. Krämer,Concepts, Syntax and Semantics of SEGRASA 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. 2548.
[32] E. Battiston, F. De Cindio, and G. Mauri, "OBJSA nets: A class of highlevel 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: SpringerVerlag, 1988, pp. 2043.
[33] W. Reisig, "Petri nets and algebraic specifications,"J. Theoret. Comput. Sci., vol. 80, pp. 134, 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: SpringerVerlag, 1987, pp. 293308.
[35] J. Billington, "Manysorted highlevel nets," inProc. 3rd Int. Workshop Petri Nets and Performance Models, Kyoto, Japan, 1989, pp. 166179, Computer Society Press.
[36] C. Dimitrovici, U. Hummert, and L. Petrucci, "Semantics, composition and net properties of algebraic highlevel nets," in G. Rozenberg, Ed.,Advances in Petri Nets 1991, no. 524 inLecture Notes in Computer Science. Berlin, Heidelberg, New York: SpringerVerlag, 1991, pp. 93117.
[37] K. Jensen, "coloured Petri nets and the invariantmethod,"J. Theoret. Comput. Sci., vol. 14, pp. 317336, 1981.
[38] K. Jensen and G. Rozenberg, Eds.HighLevel Petri Nets; Theory and Application. New York: SpringerVerlag, 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: PrenticeHall, 1978, pp. 80149.