This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Formal Specification Framework for Object-Oriented Distributed Systems
July 2000 (vol. 26 no. 7)
pp. 635-652

Abstract—In this paper, we present the Concurrent Object-Oriented Petri Nets (CO-OPN/2) formalism devised to support the specification of large distributed systems. Our approach is based on two underlying formalisms: order-sorted algebra and algebraic Petri nets. With respect to the lack of structuring capabilities of Petri nets, CO-OPN/2 has adopted the object-oriented paradigm. In this hybrid approach (model- and property-oriented), classes of objects are described by means of algebraic Petri nets, while data structures are expressed by order-sorted algebraic specifications. An original feature is the sophisticated synchronization mechanism. This mechanism allows to involve many partners in a synchronization and to describe the synchronization policy. A typical example of distributed systems, namely the Transit Node, is used throughout this paper to introduce our formalism and the concrete specification language associated with it. By successive refinements of the components of the example, we present, informally, most of the notions of CO-OPN/2. We also give some insights about the coordination layer, Context and Objects Interface Language (COIL), which is built on top of CO-OPN/2. This coordination layer is used for the description of the concrete distributed architecture of the system. Together, CO-OPN/2 and COIL provide a complete formal framework for the specification of distributed systems.

[1] P. America, ”Inheritance and Subtyping in a Parallel Object-Oriented Language,” Proc. European Conf. Object-Oriented Programming, vol. 276, pp. 234–242, June 1987.
[2] P. America, “A Behavioral Approach to Subtyping in Object-Oriented Programming Languages,” Technical Report 443, Philips Research Laboratories, Nederlandse Philips Bedrijven B.V., Apr. 1989, revised Jan. 1989.
[3] S. Barbey, D. Buchs, and C. Péraire, ”A Theory of Specification-Based Testing for Object-Oriented Software,” Proc. European Dependable Computing Conf., Technical Report (EPFL-DI-LGL no. 96/163), Oct. 1996.
[4] E. Battiston, A. Chizzoni, and F. De Cindio, ”Modeling a Cooperative Environment with CLOWN,” Proc. Second Int'l Workshop Object-Oriented Programming and Models of Concurrency within the 16th Int'l Conf. Application and Theory of Petri Nets, pp. 12–24, June 1996.
[5] G. Berry and G. Gonthier, “The Esterel Synchronous Programming Language: Design, Semantics, Implementation,” technical report, INRIA, 1988.
[6] O. Biberstein, “CO-OPN/2: An Object-Oriented Formalism for the Specification of Concurrent Systems,” PhD thesis, University of Geneva, July 1997.
[7] O. Biberstein, D. Buchs, and N. Guelfi, “Object-Oriented Nets with Algebraic Specifications: The CO-OPN/2 Formalism,” Advances in Petri Nets on Object-Orientation, G. Agha and F. De Cindio, eds., Springer-Verlag, 2000.
[8] D. Buchs, P. Racloz, M. Buffo, J. Flumet, and E. Urland, ”Deriving Parallel Programs Using SANDS Tools,” Transputer Comm., vol. 3, no. 1, pp. 23–32, Jan. 1996.
[9] D. Buchs and N. Guelfi, ”CO-OPN: A Concurrent Object-Oriented Petri Nets Approach for System Specification,” Proc. 12th Int'l Conf. Application and Theory of Petri Nets, pp. 432–454, June 1991.
[10] D. Buchs and N. Guelfi, ”Formal Development of Actor Programs Using Structured Algebraic Petri Nets,” Proc. Int'l Conf. Parallel Architectures and Languages Europe (PARLE), vol. 694, pp 353–366, June 1993.
[11] D. Buchs and J. Hulaas, ”Evolutive Prototyping of Heterogeneous Distributed Systems Using Hierarchical Algebraic Petri Nets,” Proc. Int'l Conf. Systems, Man and Cybernetics, Oct. 1996.
[12] D. Buchs, F. Mourlin, and L. Safavi, ”CO-OPN for Specifying a Distributed Termination Detection Algorithm,” World Transputer Congress, Workshop on Software Engineering for Parallel Systems, vol. 3, pp. 25–29, Sept. 1993.
[13] M. Buffo and D. Buchs, ”A Coordination Model for Distributed Object Systems,” Proc. Second Int'l Conf. Coordination Models and Languages (COORDINATION), vol. 1,282, pp. 410–413, 1997.
[14] G. Di Marzo Serugendo and N. Guelfi, ”Using Object-Oriented Algebraic Nets for the Reverse Engineering of Java Programs: A Case Study,” Proc. Int'l Conf. Application of Concurrency to System Design (CSD), Technical Report (EPFL-DI no. 98/267), IEEE CS Press, 1998.
[15] J.A. Goguen and J. Meseguer, ”Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions, and Partial Operations,” Theoretical Computer Science, Technical Report SRI-CSL-89-10 (1989), Computer Science Lab., SRI International, vol. 105, no. 2, pp. 217–273, 1992.
[16] N. Guelfi, O. Biberstein, D. Buchs, E. Canver, M-C. Gaudel, F. von Henke, and D. Schwier, Comparison of Object-Oriented Formal Methods, technical report of the Esprit Long Term Research Project 20072, “Design For Validation,” University of Newcastle Upon Tyne, Department of Computing Science, 1997.
[17] D. Harel, “Statecharts: A Visual Approach to Complex Systems,” Science of Computer Programming, Vol. 8, No. 3, pp. 231–274, 1987.
[18] C.A. Lakos, ”The Object Orientation of Object Petri Nets,” Proc. First Int'l Workshop Object-Oriented Programming and Models of Concurrency within the 16th Int'l Conf. Application and Theory of Petri Nets, pp. 1–14, June 1995.
[19] C.A. Lakos, ”The Consistent Use of Names and Polymorphism in the Definition of Object Petri Nets,” Proc. Application and Theory of Petri Nets, vol. 1,091, pp. 380–399, June. 1996
[20] B. Liskov and J.M. Wing, ”A Behavioral Notion of Subtyping,” ACM Trans. Programming Languages and Systems, vol. 16, no. 6, pp. 1,811–1,841, Nov. 1994.
[21] G. Di Marzo, “Stepwise Refinement of Formal Specifications Based on Logical Formulae: From CO-OPN/2 Specifications to Java Programs,” PhD thesis, no. 1931, Ecole Polytechnique Fdrale de Lausanne, Dpartement d'Informatique, 1015 Lausanne, Switzerland, Jan. 1999.
[22] S. Mauw and F. Wiedijk, ”Specification of the Transit Node in${\rm PSF}_d$,” Algebraic Methods II: Theory, Tools and Applications, J.A. Bergstra and L.M.G. Feijs, eds., vol. 490, Vrije Univ., Springer Verlag, pp. 340–361, 1991.
[23] M. Bidoit, M.-C. Gaudel, J. Hagelstein, A. Mauboussin, and H. Perdrix, ”From An ERAE Requirements Specification to a PLUSS Algebraic Specification: A Case Study,” Algebraic Methods II: Theory, Tools and Applications, J.A. Bergstra and L.M.G. Feijs, eds., Vrije Univ., Springer Verlag, vol. 490, pp. 395–397, 1991.
[24] W. Reisig, ”Petri Nets and Algebraic Specifications,” Theoretical Computer Science, vol. 80, pp. 1–34, 1991.
[25] C. Sibertin-Blanc, ”Cooperative Nets,” Proc. 15th Int'l Conf., Application and Theory of Petri Nets, R. Valette, ed., vol. 815, pp. 471–490, June 1994.
[26] A. Snyder, ”Encapsulation and Inheritance in Object-Oriented Programming Languages,” Proc. Object-Oriented Programming Languages and Applications, ACM SIGPLAN Notices, vol. 21, no 11, pp. 38–45, Nov. 1986.

Index Terms:
Formal specifications, object-orientation, distributed systems, concurrency, algebraic Petri nets, refinement, subtyping, algebraic specifications.
Citation:
Didier Buchs, Nicolas Guelfi, "A Formal Specification Framework for Object-Oriented Distributed Systems," IEEE Transactions on Software Engineering, vol. 26, no. 7, pp. 635-652, July 2000, doi:10.1109/32.859532
Usage of this product signifies your acceptance of the Terms of Use.