A formal specification framework for object-oriented distributedsystems

摘要

In this paper, we present the Concurrent Object-Oriented PetrinNets (CO-OPN/2) formalism devised to support the specification of largendistributed systems. Our approach is based on two underlying formalisms:norder-sorted algebra and algebraic Petri nets. With respect to the lacknof structuring capabilities of Petri nets, CO-OPN/2 has adopted thenobject-oriented paradigm. In this hybrid approach (model- andnproperty-oriented), classes of objects are described by means ofnalgebraic Petri nets, while data structures are expressed bynorder-sorted algebraic specifications. An original feature is thensophisticated synchronization mechanism. This mechanism allows toninvolve many partners in a synchronization and to describe thensynchronization policy. A typical example of distributed systems, namelynthe Transit Node, is used throughout this paper to introduce ournformalism and the concrete specification language associated with it. Bynsuccessive refinements of the components of the example, we present,ninformally, most of the notions of CO-OPN/2. We also give some insightsnabout the coordination layer, Context and Objects Interface Languagen(COIL), which is built on top of CO-OPN/2. This coordination layer isnused for the description of the concrete distributed architecture of thensystem. Together, CO-OPN/2 and COIL provide a complete formal frameworknfor the specification of distributed systems