|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
| ASCII Text | x | ||
| 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. | |||
| BibTex | x | ||
| @article{ 10.1109/32.859532, author = {Didier Buchs and Nicolas Guelfi}, title = {A Formal Specification Framework for Object-Oriented Distributed Systems}, journal ={IEEE Transactions on Software Engineering}, volume = {26}, number = {7}, issn = {0098-5589}, year = {2000}, pages = {635-652}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.859532}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - JOUR JO - IEEE Transactions on Software Engineering TI - A Formal Specification Framework for Object-Oriented Distributed Systems IS - 7 SN - 0098-5589 SP635 EP652 EPD - 635-652 A1 - Didier Buchs, A1 - Nicolas Guelfi, PY - 2000 KW - Formal specifications KW - object-orientation KW - distributed systems KW - concurrency KW - algebraic Petri nets KW - refinement KW - subtyping KW - algebraic specifications. VL - 26 JA - IEEE Transactions on Software Engineering ER - | |||
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
[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.