Using the COOPN/2 Formal Method for Groupware Systems Engineering

1996
Conference paper

COOPN/2 (Concurrent Object Oriented Petri Nets) is an object-oriented specification formalism based on Petri Nets and algebraic specifications. It is fully adapted to the specification of complex concurrent systems because it inherits the advantages of algebraic specifications for the specification of abstract data types, from Petri nets to describe partially ordered events and from the object-oriented paradigm for the 'structuring' of the specification. All these features are especially useful when speaking about groupware systems, which are application which demand rich modeling capabilities on concurrency and structuring. This paper explains the major principles for the specification of groupware systems with COOPN/2. This is done by mapping groupware concepts into COOPN/2 concepts and is demonstrated by means of an example of shared distributed diaries. Furthermore, we present the work done on the methodological approach for the development of concurrent object-oriented systems with COOPN/2 which cover analysis, specification, design, prototyping and testing. groupware, replication, object-orientation, distributed systems, formal methods, Petri Nets, algebraic specification of abstract data types, software engineering. Keywords : groupware, replication, object-orientation, distributed systems, formal methods, Petri Nets, algebraic specification of abstract data types, software engineering.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related concepts

Related publications

1996
Conference paper

Abstract

Official source

https://infoscience.epfl.ch/record/54574?ln=en

About this result

Related concepts (9)

Related concepts

Related publications (19)

Related publications

Petri net

A Petri net, also known as a place/transition (PT) net, is one of several mathematical modeling languages for the description of distributed systems. It is a class of discrete event dynamic system.

Formal methods

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods f

System

A system is a group of interacting or interrelated elements that act according to a set of rules to form a unified whole. A system, surrounded and influenced by its environment, is described by its

Formal Development of Actor Programs using Structured Algebraic Petri Nets

This paper provides with an actor semantics using a formalism called CO-OPN (Concurrent Object Oriented Petri Nets) which is modular and incorporates both concurrency and data structuring features. Actor languages are the main model of concurrent object oriented languages, but they are rarely well formalized. CO-OPN is a structured extension of Petri nets and algebraic abstract data types. A CO-OPN specification is composed of a set of objects (algebraic abstract data types and Petri nets), and of a synchronous communication mechanism. These synchronisation mechanism are defined in order to keep object state encapsulation, allowing to specify independantly each object. The translation of an actor program into a CO-OPN specification is done by building objects for actors. The adequacy of CO-OPN to describe the semantics of concurrent object oriented languages is shown by this formal semantic description of actor languages. Some particular implementations are suggested, improving the concurrency of executions of actor programs. Keywords : Specification and verification, Formal program development methodologies, modular specification, semantics, actor languages semantics, high level Petri nets, algebraic abstract data types.

1993

In this article we present the concurrent object-oriented specification language COOPN/2 which extends the COOPN (Concurrent Object Oriented Petri Nets) formalism, destined to support the development of large heterogenous distributed systems. The development of distributed applications has recently been the subject of intensive research, due to potential benefits that can be expected to offer in increasing reliability and overall performance of computer processing. One way of improving the effectiveness of the distributed system construction is to adopt a rigorous approach for system development, based on structuring principles. The COOPN/2 approach proposes a specification language, based on the object-oriented paradigm, which includes a fine description of true concurrent behaviors. This hybrid approach (model and property-oriented) allows for a description of the concurrent aspects through the use of a high-level Petri nets formalism which includes data structures expressed with the algebraic abstract data types and a synchronization mechanism for building hierarchies of abstraction. This latter notion is the concept which is used in structuring applications. Interesting properties of COOPN, such as the progressive refinement of specifications, allow for the building of systems in an incremental manner.In this article, we introduce COOPN/2 informally, by means of a typical example of distributed systems, the transit node, in order to introduce each useful and innovative mechanism of the language. Then, in the context of distributed software engineering with COOPN/2, we present our current works done in order to provide formal methods for several steps of a life cycle model test, prototyping, analysis,....). Keywords: software engineering, formal specification language, refinement, prototyping, distributed systems, object orientation, concurrency, Petri nets, algebraic specification.

1996

Formal Development of Java Programs

The Java object-oriented programming language has been the subject of an important involvement from programmers and industry. Especially for applications related to the Web. The problem of such rapid penetration of Java programs into commercial product is that software engineers does not have any methodology and have to develop complex parallel applications. In this paper, we present, using a real (http://lglsun.epfl.ch/Team/GDM/DSGamma.html) but simple Web parallel application, a possible formal development methodology based on the stepwise refinement of CO-OPN/2 formal specifications. The application chosen is based on the Gamma paradigm, in which additions are realized across distributed multisets of integers maintained by local Java applets. CO-OPN/2 is an object-oriented specification formalism allowing the formal specification of abstract data types based on algebraic specification and of concurrent objects using a Petri net like approach. An interesting feature of CO-OPN/2 is that it gives a coherent solution for the expression of complex properties combining inheritance, concurrency and synchronizations. The refinement of formal descriptions for building progressively the Java program is presented in several refinement steps. This refinement process focuses on the distribution of data and treatments, and validation and verification are studied through the refinement of system properties.

1997