CO-OPN/2: An Object-Oriented Formalism for the Specification of Concurrent Systems

In this thesis we formally define the syntactic and semantic aspects of the object-oriented formalism, called CO-OPN/2 (Concurrent Object-Oriented Petri Nets), which is devised for the specification and the modeling of large concurrent systems. Moreover, we propose a concrete specification language which supports the formalism and which is used in numerous examples. CO-OPN/2 belongs to the category of algebraic nets, i.e. a powerful combination of algebraic specifications and Petri nets. The former underlying formalism is used to describe the data structures and the functional aspects of a system, while the latter serves to model its operational and concurrent features. Our approach fully integrates the most important notions specific to object orientation: encapsulation, class of objects, dynamic creation/destruction, concurrency, subtyping, and inheritance. The original and innovative features of CO-OPN/2 are its sophisticated synchronization mechanism, the definition of subtyping based on bisimulation, and the explicit distinction between inheritance and subtyping. A static and a dynamic semantics of the formalism are provided. As for the dynamic semantics, it consists in a step semantics expressed in terms of transition systems and constructed by means of a set inference rules. These inference rules have been designed to deal differently with internal and external object events. In addition, special care has been directed to provide the maximal flexibility concerning the dynamic creation/destruction and the concurrency. Finally, in order to demonstrate the adequacy of our approach we adopted a common case study. This case study deals with the specification of a collaborative editor of structured diagrams.