Formal Treatment of Data Structures in Concurrency Models

The problem of real size system modelling with basic concurrency models like transition systems, Petri nets or process algebra is that there is no possibility to model easily the system data structures. Algebraic specification is a method well adapted to this last aspect and has been chosen to be mixed with the two major concurrency models which are process algebra and Petri nets. We present in this paper how the 'mixing' is done and what are the consequences concerning concurrency through the case of Lotos and Algebraic nets. Our approach is built on a simple case study which is given in several versions with both formalisms. The first one uses the basic models without algebraic specifications to highlight the data structures modelling problem. The second one is used to present how algebraic specifications are integrated in each concurrency model and the last one focuses on the concurrency aspects. Several propositions are then given in order to enhance the mixing of algebraic specifications and Petri nets or process algebra. Keywords : Petri net, process algebra, data types, algebraic specification, algebraic net, Lotos.

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

COOPN/2 : A Specification Language for Distributed Systems Engineering

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

Using the COOPN/2 Formal Method for Groupware Systems Engineering

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.

1996