Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. EPFL thesis
  4. CO-OPN/2: An Object-Oriented Formalism for the Specification of Concurrent Systems
 
doctoral thesis

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

Biberstein, Olivier
1997

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.

  • Details
  • Metrics
Type
doctoral thesis
Author(s)
Biberstein, Olivier
Advisors
Zanella, Paolo
Date Issued

1997

Publisher

Université de Genève

Subjects

formal specification

•

nets

•

concurrency

•

formal methods

•

subtyping

EPFL units
LGL  
Available on Infoscience
September 20, 2005
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/216844
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés