This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Modular Algebraic Nets to Specify Concurrent Systems
October 1996 (vol. 22 no. 10)
pp. 689-705

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 high-level 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 user-oriented introduction, the definition of OBJSA nets (as subclass of SPEC-inscribed 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, "ACT-ONE: An Algebraic Specification Language with Two Level of Semantics," TR 83-01, Technical Univ. Berlin, 1983.
[3] J.A. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J.-P. Jouannaud, "Introducing OBJ3," Report SRI-CSL-92-03, SRI Int'l, Computer Science Lab, 1992.
[4] W. Reisig, “Petri Nets—An Introduction,” EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 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. Springer-Verlag, 1980.
[7] J.A. Bergstra and J.W. Klop, "Process Algebra for Synchronous Communication," Information&Control, vol. 60, nos. 1/3, pp. 109-137, 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. 1-39. Springer-Verlag, 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. Springer-Verlag, 1987.
[10] The Formal Description Technique LOTOS, P.H.J. Van Eijk, C.A. Vissers and M. Diaz, eds. North-Holland, 1989.
[11] J. Meseguer, "Conditional Rewriting Logic as a Unified Model of Concurrency," Theoretical Computer Science, vol. 96, pp. 73-155 1992.
[12] H.J. Genrich and K. Lautenbach, "System Modeling with High-Level Petri Nets," TCS 13, pp. 109-136, 1981. Also in [26].
[13] K. Jensen, "Coloured Petri Nets and the Invariant Method," Theoretical Computer Science, vol. 14, pp. 317-336, 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. 192-209,Bonn, Germany, 1989.
[15] G. Bruno and G. Marchetto, "Process-Translatable 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 High-Level Petri Net Formalism for Time-Critical 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. 269-286. Springer-Verlag, 1987. Also in [26].
[18] B. Kramer, Concepts, Syntax and Semantics of SEGRAS, GM-Bericht 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. 293-308. Springer-Verlag, 1987.
[20] C. Dimitrovici, U. Hummert, and L. Petrucci, "Semantics, Composition and Net Properties of Algebraic High-Level Nets," Advances in Petri Nets 1991, G. Rozenberg, ed., Lecture Notes On Computer Science 524, pp. 93-117. Springer-Verlag, 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. 188-206. Springer-Verlag, 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. 20-43. Springer-Verlag, 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, June26-28, 1991.
[24] J. Billington, "Many-Sorted High-Level Nets," Proc. Third Int'l Workshop Petri Nets and Performance Models, pp. 166-179,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. Springer-Verlag, 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. Springer-Verlag, 1982.
[28] J.A. Goguen and J. Meseguer, "Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations," Report SRI-CSL-89-10, SRI Int'l, Computer Science Lab., 1989.
[29] J.A. Goguen, "Parameterized Programming," IEEE Trans. Software Eng., vol. 10, no. 5, pp. 528-543, 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. 84-102. Springer-Verlag, 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. Moller-Pedersen, 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. 666-677, 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. 304-351. Springer-Verlag, 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, "Net-Based Description of Parallel Object-Based Systems or POTS and POPS," Foundations of Object-Oriented Languages, REX School/Workshop, J.W. de Bakker, W.P. de Roever, and G. Rozenberg, eds., Lecture Notes On Computer Science 489. Springer-Verlag, 1991.
[39] W. Reisig, "Place/Transitions Systems," Advances in Petri Nets 1988, G. Rozenberg, ed., Lecture Notes On Computer Science 254, pp. 1-46. Springer-Verlag, 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. 269-286. Springer-Verlag, 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. Springer-Verlag, 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. Springer-Verlag, 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. 93-122, 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. Wilbur-Ham, "PROTEAN: A High-Level Petri Net Tool for the Specification and Verification of Communication Protocols," IEEE Trans. Software Eng., vol. 14, no. 3, pp. 301-316, 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 Real-Time Systems," Report no. 54-94, 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. Maggiolo-Schettini, 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. 47-76, Franco Angeli, 1995 (in Italian).
[54] R. De Nicola, A. Fantechi, S. Gnesi, and G. Ristori, "An Action-Based Framework for Verifying Logical and Behavioural Properties of Concurrent Systems," Computer Network and ISDN Systems, vol. 25, no. 7, pp. 761-778, 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. 1-46. Springer-Verlag, 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. 391-411. Springer-Verlag, 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. 238-257. Springer-Verlag, 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 State-Space Verification methods," Applications and Theory of Petri Nets 1996, J. Billington and W. Reisig, eds., Lecture Notes On Computer Science 1091, pp. 29-56. Springer-Verlag, 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 High-Level Petri Nets," Application and Theory of Petri Nets 1995, G. De Michelis and M. Diaz, eds., Lecture Notes On Computer Science 935, pp. 103-120. Springer-Verlag, 1995.
[62] Proc. First Workshop Object-Oriented Programming and Models of Concurrency, G. Agha and F. De Cindio, eds., Turin, Italy, June 1995.
[63] Proc. Second Workshop Object-Oriented Programming and Models of Concurrency, G. Agha and F. De Cindio, eds., Osaka, Japan, June 1996.

Index Terms:
Formal specification, distributed systems, Petri nets, OBJ, compositionality, environments.
Citation:
Eugenio Battiston, Fiorella De Cindio, Giancarlo Mauri, "Modular Algebraic Nets to Specify Concurrent Systems," IEEE Transactions on Software Engineering, vol. 22, no. 10, pp. 689-705, Oct. 1996, doi:10.1109/32.544348
Usage of this product signifies your acceptance of the Terms of Use.