
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Eugenio Battiston, Fiorella De Cindio, Giancarlo Mauri, "Modular Algebraic Nets to Specify Concurrent Systems," IEEE Transactions on Software Engineering, vol. 22, no. 10, pp. 689705, October, 1996.  
BibTex  x  
@article{ 10.1109/32.544348, author = {Eugenio Battiston and Fiorella De Cindio and Giancarlo Mauri}, title = {Modular Algebraic Nets to Specify Concurrent Systems}, journal ={IEEE Transactions on Software Engineering}, volume = {22}, number = {10}, issn = {00985589}, year = {1996}, pages = {689705}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.544348}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Modular Algebraic Nets to Specify Concurrent Systems IS  10 SN  00985589 SP689 EP705 EPD  689705 A1  Eugenio Battiston, A1  Fiorella De Cindio, A1  Giancarlo Mauri, PY  1996 KW  Formal specification KW  distributed systems KW  Petri nets KW  OBJ KW  compositionality KW  environments. VL  22 JA  IEEE Transactions on Software Engineering ER   
Abstract—In this paper, we present the basic features of a specification language for concurrent distributed systems, developed at the Department of Information Sciences of the University of Milan, Italy. The language is based on a class of modular algebraic highlevel nets, OBJSA nets, which result from the synthesis of Superposed Automata (SA) nets and of the algebraic specification language OBJ. It is supported by the OBJSA Net Environment (ONE).
OBJSA nets stress the possibility of building the system model by composing its components and encourage the incremental development of the specification and its reusability. An OBJSA net consists of an SA net inscribed with terms of an OBJ module. The ONE environment supports the user in producing and executing a specification, hiding from her/him, as much as possible, the technical details of the algebraic part of the specification.
The paper provides a complete presentation of OBJSA nets, including a useroriented introduction, the definition of OBJSA nets (as subclass of SPECinscribed nets), of their occurrence rule (the semantics) and of the composition operation. In addition it presents the kernel of the support environment.
[1] D. Bjorner and C.B. Jones, Formal Specification and Software Development. Prentice Hall, 1982.
[2] H. Ehrig, W. Fey, and H. Hansen, "ACTONE: An Algebraic Specification Language with Two Level of Semantics," TR 8301, Technical Univ. Berlin, 1983.
[3] J.A. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J.P. Jouannaud, "Introducing OBJ3," Report SRICSL9203, SRI Int'l, Computer Science Lab, 1992.
[4] W. Reisig, “Petri Nets—An Introduction,” EATCS Monographs on Theoretical Computer Science. SpringerVerlag, vol. 4, 1985.
[5] T. Murata, “Petri Nets: Properties, Analysis and Application,” Proc. IEEE, vol. 77, no. 4, 1989.
[6] R. Milner, A Calculus for Communicating Systems, Lecture Notes On Computer Science 92. SpringerVerlag, 1980.
[7] J.A. Bergstra and J.W. Klop, "Process Algebra for Synchronous Communication," Information&Control, vol. 60, nos. 1/3, pp. 109137, 1984.
[8] E. Astesiano and G. Reggio, "Algebraic Specification of Concurrency," Recent Trends in Data Type Specification, M. Bidoit and C. Choppy, eds., Lecture Notes On Computer Science 655, pp. 139. SpringerVerlag, 1993.
[9] E. Astesiano and G. Reggio, "An Outline of the SMoLCS Approach," Mathematical Models for Semantics of Parallelism, Lecture Notes On Computer Science 280. SpringerVerlag, 1987.
[10] The Formal Description Technique LOTOS, P.H.J. Van Eijk, C.A. Vissers and M. Diaz, eds. NorthHolland, 1989.
[11] J. Meseguer, "Conditional Rewriting Logic as a Unified Model of Concurrency," Theoretical Computer Science, vol. 96, pp. 73155 1992.
[12] H.J. Genrich and K. Lautenbach, "System Modeling with HighLevel Petri Nets," TCS 13, pp. 109136, 1981. Also in [26].
[13] K. Jensen, "Coloured Petri Nets and the Invariant Method," Theoretical Computer Science, vol. 14, pp. 317336, 1981. Also in [26].
[14] P. Huber, K. Jensen, and R. Shapiro, "Hierarchies in Coloured Petri Nets," Proc. 10th Int'l Conf. Applications and Theory of Petri Nets 1989, pp. 192209,Bonn, Germany, 1989.
[15] G. Bruno and G. Marchetto, "ProcessTranslatable Petri Nets for the Rapid Prototyping of Process Control Systems," IEEE Trans. Software Eng., vol. 12, no. 2, Feb. 1986.
[16] C. Ghezzi, D. Mandrioli, S. Morasca, and M. Pezze, “A Unified HighLevel Petri Net Formalism for TimeCritical Systems,” IEEE Trans. Software Eng., vol. 17, no. 2, pp. 160–171, Feb. 1991.
[17] B. Kramer and H.W. Schmidt, "Types and Modules for Net Specifications," Concurrency and Nets, K. Voss, H. Genich, and G. Rozenberg, eds., pp. 269286. SpringerVerlag, 1987. Also in [26].
[18] B. Kramer, Concepts, Syntax and Semantics of SEGRAS, GMBericht nr. 179, R. Oldenbourg Verlag, 1989.
[19] J. Vautherin, "Parallel Systems Specification with Colored Petri Nets and Algebraic Specification," Advances in Petri Nets 1987, G. Rozenberg, ed., Lecture Notes On Computer Science 266, pp. 293308. SpringerVerlag, 1987.
[20] C. Dimitrovici, U. Hummert, and L. Petrucci, "Semantics, Composition and Net Properties of Algebraic HighLevel Nets," Advances in Petri Nets 1991, G. Rozenberg, ed., Lecture Notes On Computer Science 524, pp. 93117. SpringerVerlag, 1991.
[21] H. Ehrig, J. Padberg, and L. Ribeiro, "Algebraic High Level Nets: Petri Nets Revisitated," Recent Trends in Data Type Specification, H. Ehrig and F. Orejas, eds., Lecture Notes on Computer Science 785, pp. 188206. SpringerVerlag, 1992.
[22] E. Battiston, F. De Cindio, and G. Mauri, "OBJSA Nets: A Class of High Level Nets Having Objects as Domains," Advances in Petri Nets 1988, G. Rozenberg, ed., Lecture Notes On Computer Science 340, pp. 2043. SpringerVerlag, 1988. Also in [26].
[23] E. Battiston, F. De Cindio, G. Mauri, and L. Rapanotti, "Morphisms and Minimal Models for OBJSA Nets," Proc. 12th Int'l Conf. Application and Theory of Petri Nets,Gjern, Denmark, June2628, 1991.
[24] J. Billington, "ManySorted HighLevel Nets," Proc. Third Int'l Workshop Petri Nets and Performance Models, pp. 166179,Kyoto, 1989. Also in [26].
[25] W. Reisig, ”Petri Nets and Algebraic Specifications,” Theoretical Computer Science, vol. 80, pp. 1–34, 1991.
[26] High Level Petri Nets. Theory and Application. K. Jensen and G. Rozenberg, eds. SpringerVerlag, 1991.
[27] F. De Cindio, G. De Michelis, L. Pomello, and C. Simone, "Superposed Automata Nets," Application and Theory of Petri Nets, C. Girault, and W. Reisig, eds., IFB 52. SpringerVerlag, 1982.
[28] J.A. Goguen and J. Meseguer, "OrderSorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations," Report SRICSL8910, SRI Int'l, Computer Science Lab., 1989.
[29] J.A. Goguen, "Parameterized Programming," IEEE Trans. Software Eng., vol. 10, no. 5, pp. 528543, 1984.
[30] T. Winkler, Introducing OBJ3's New Features, Manual of the Release 2.0 of the OBJ3 Interpreter. SRI Int'l, Computer Science Lab., 1992.
[31] E. Battiston, O. Botti, E. Crivelli, and F. De Cindio, "An Incremental Specification of a Hydroelectric Power Plant Control System Using a Class of Modular Algebraic Nets," Application and Theory of Petri Nets 1995, G. De Michelis and M. Diaz, eds., Lecture Notes On Computer Science 935, pp. 84102. SpringerVerlag, 1995.
[32] T. Winograd, "Beyond Programming Languages," Comm. ACM, vol. 22, no. 7, July 1979.
[33] G.M. Birtwistle, O.J. Dahl, B. Myrhaug, and K. Nygaard, "Simula Begin, Studentlitteratur," Lund and Auerbach Publishers, 1973.
[34] B.B. Kristensen, O.L. Madsen, B. MollerPedersen, and K. Nygaard, "The BETA Programming Language," Research Directions in Object Oriented Programming, B.D. Shriver and P. Wegner, eds. MIT Press, 1987.
[35] C.A.R. Hoare,“Communicating sequential processes,” Comm. of the ACM, vol. 21, no. 8, pp. 666677, Aug. 1978.
[36] L. Bernardinello and F. De Cindio, "A Survey of Basic Net Models and Modular Net Classes," Advances in Petri Nets 1992, G. Rozenberg, ed., Lecture Notes On Computer Science 609, pp. 304351. SpringerVerlag, 1992.
[37] E. Battiston, A. Chizzoni, and F. De Cindio, "Inheritance and Concurrency in CLOWN," in [62], 1995.
[38] J. Engelfriet, G. Leih, and G. Rozenberg, "NetBased Description of Parallel ObjectBased Systems or POTS and POPS," Foundations of ObjectOriented Languages, REX School/Workshop, J.W. de Bakker, W.P. de Roever, and G. Rozenberg, eds., Lecture Notes On Computer Science 489. SpringerVerlag, 1991.
[39] W. Reisig, "Place/Transitions Systems," Advances in Petri Nets 1988, G. Rozenberg, ed., Lecture Notes On Computer Science 254, pp. 146. SpringerVerlag, 1987.
[40] W. Reisig and E. Smith, "The Semantics of a Net Is a Net: An Exercise in General Net Theory," Concurrency and Nets, K. Voss, H. Genrich, and G. Rozenberg, eds., pp. 269286. SpringerVerlag, 1987.
[41] E. Battiston, V. Crespi, F. De Cindio, and G. Mauri, "Sematics Frameworks for a Class of Modular Algebraic Nets," Proc. Third Int'l Conf. Algebraic Methodology and Software Technology AMAST '93, M. Nivat, C. Rattay, R. Su, G. Scollo, eds., Workshops in Computing. SpringerVerlag, 1993.
[42] J. Meseguer and U. Montanari, "Petri Nets Are Monoids," Information&Computation. Vol. 88, no. 2, 1990.
[43] K. Jensen, Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use, vol. 1, Basic Concepts. Monographs in Theoretical Computer Science. SpringerVerlag, 1997.
[44] K. Jensen et al., DesignCPN: A Reference Manual.Cambridge, Mass.: Meta Software Co., 1991.
[45] M.Ajmone Marsan,G. Balbo,, and G. Conte,“A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems,” ACM Trans. Computer Systems, pp. 93122, vol. 2, no. 2, May 1984.
[46] G. Chiola, "A Graphical Petri Net Tool for Performance Analysis," Proc. Third Int'l Workshop Modeling Techniques and Performance Evaluation, AFCET, Paris, 1987.
[47] F.J.W. Symons, "Modelling and Analysis of Communication Protocols Using Numerical Petri Nets," PhD dissertation, Dept. of Electrical Eng. Science, Univ. of Essex, Telecommunications Systems Group Report 152, May 1978.
[48] J. Billington, G.R. Wheeler, and M.C. WilburHam, "PROTEAN: A HighLevel Petri Net Tool for the Specification and Verification of Communication Protocols," IEEE Trans. Software Eng., vol. 14, no. 3, pp. 301316, Mar. 1988. Also in [26].
[49] M. Baldassarri and G. Bruno,“Protob: An object oriented methodology for developing discrete dynamicsystems,” Computer Languages, vol. 16, no. 1, 1991.
[50] M. Pezzè, "CABERNET: A customizable Environment for the Specification and Analysis of RealTime Systems," Report no. 5494, Politecnico di Milano, Dip. di Elettronica e Informatica, June 1994.
[51] J. Halhotra, DesignML, Reference Manual.Cambridge, Mass.: Meta Software Co., 1990.
[52] R. Milner,M. Tofte,, and R. Harper,The Definition of Standard ML.Cambridge, Mass.: MIT Press, 1990.
[53] E. Astesiano, E. Battiston, F. De Cindio, R. De Nicola, S. Gnesi, A. MaggioloSchettini, and G. Reggio, "Metodologie e Strumenti per la Specifica e la Verifica di Sistemi Concorrenti," Ambienti per Linguaggi di Nuoa Concezione, G. Filè, ed., Collana CNR, Progetto Finalizzato "Sistemi Informatici e Calcolo Parallelo," pp. 4776, Franco Angeli, 1995 (in Italian).
[54] R. De Nicola, A. Fantechi, S. Gnesi, and G. Ristori, "An ActionBased Framework for Verifying Logical and Behavioural Properties of Concurrent Systems," Computer Network and ISDN Systems, vol. 25, no. 7, pp. 761778, NorthHolland, 1993.
[55] W. Brauer, R. Gold, and W. Vogler, "Behaviour and Equivalences Preserving Refinements of Petri Nets," Advances in Petri Nets 1990, G. Rozenberg, ed., Lecture Notes On Computer Science 483, pp. 146. SpringerVerlag, 1990.
[56] K. Schmidt, "Parameterized Reachability Trees for Algebraic Petri Nets," Application and Theory of Petri Nets 1995, G. De Michelis and M. Diaz, eds., Lecture Notes On Computer Science 935, pp. 391411. SpringerVerlag, 1995.
[57] S. Haddad, J.M. Ilié, M. Taghelit, and B. Zouari, "Symbolic Reachability Trees and Partial Symmetries," Application and Theory of Petri Nets 1995, G. De Michelis and M. Diaz, eds., Lecture Notes On Computer Science 935, pp. 238257. SpringerVerlag, 1995.
[58] S. Christensen and L. Petrucci, “Modular State Space Analysis of Coloured Petri Nets,” Proc. 16th Int'l Conf. Application and Theory of Petri Nets, June 1995.
[59] A. Valmari, "Compositionality in StateSpace Verification methods," Applications and Theory of Petri Nets 1996, J. Billington and W. Reisig, eds., Lecture Notes On Computer Science 1091, pp. 2956. SpringerVerlag, 1996.
[60] M. Lindqvist, "Parameterized Reachability Trees for Predicate/Transition Nets," Proc. 11th Int'l Conf. Application and Theory of Petri Nets,Paris, June 1990.
[61] E. Best, H. Fleischhack, W. Fraczak, R.P. Hopkins, H. Klaudel, and E. Pelz, "A Class of Composable HighLevel Petri Nets," Application and Theory of Petri Nets 1995, G. De Michelis and M. Diaz, eds., Lecture Notes On Computer Science 935, pp. 103120. SpringerVerlag, 1995.
[62] Proc. First Workshop ObjectOriented Programming and Models of Concurrency, G. Agha and F. De Cindio, eds., Turin, Italy, June 1995.
[63] Proc. Second Workshop ObjectOriented Programming and Models of Concurrency, G. Agha and F. De Cindio, eds., Osaka, Japan, June 1996.