Object-Oriented Specification and Design of Concurrent Systems
by Didier Buchs and Nicolas Guelfi
The ConForM group at the Software engineering laboratory of the Swiss Federal Institute of Technology in Lausanne is involved in a project directed towards the formal development of concurrent or distributed systems by means of object-oriented techniques. This project proposes a formal specification language called CO-OPN: Concurrent Object Oriented Petri Nets. Behavioural concurrency aspects and data-structures are supported by adequate formalisms which are Petri Nets and Algebraic Abstract Data Types. Techniques for producing implementation by transformation and refinement as well as techniques for producing test sets have been developed. Tools have been built to support this formalism and are namely a graphical editor, a compiler, a test set generator and a simulator for prototyping specifications.
The activity of our team is directed towards the development of methods, techniques and tools for the formal construction of large, complex and reliable distributed systems.
Distributed systems are the most challenging and the most complex kind of systems that are practically developed. Such kind of systems needs well adapted and easy to use formal models. The inherent complexity and non-determinism of distributed systems needs well founded models, supported by tools sustaining all the different activities of the development process.
Complexity management is necessary to cope with real systems development. It can be controlled if sub-components can be separately studied for validation and implementation purposes. Reusability can be achieved only if the integration of implemented components is facilitated in the development process by the adoption of precise description interfaces and by implementation integration facilities made by proper composition mechanism.
The research project performed in our laboratory emphasis on four main activities, which are: system modelling, system implementation, system verification and validation and development of supporting tools. The objective of the project is the integration of research results in these activities into a common framework, which is here the CO-OPN language (Concurrent Object Oriented Petri Nets).
System Modelling
Structuring is the key notion of system partitioning destined to manage the complexity of real systems. Object-orientation is now a well accepted principle, based on encapsulation and abstraction principles, that can be used for the clear and natural separation of system components as well as the classification of such components. We are working on new concepts of object orientation, such as observational subtyping, that we introduced in the CO-OPN specification language. We are also interested in the development of particular semantics reducing the complexity of the process of property verification.
System Implementation
The main principle exploited as implementation technique is the incremental prototyping method which consists of using hierarchies of classes for the progressive realization of an implementation. Abstract classes are used to describe the automatically generated codes based on the operational semantics of the specification language. The abstract semantics of CO-OPN introduce high-level synchronization concepts: We will introduce a new equivalent operational semantics, which will be based on multilevel nested transactions. This principle is a new operational paradigm, different from classical message passing models, and which is very powerful at the modelling stage.
System Verification
The use of a well defined refinement process, allowed by our formal model, is a way to the improvement of reliability of the systems under development. The refinement process must automatically integrate incremental inclusion of correct implementations, which is the purpose of evolutionary prototyping.
We are also developing formal testing methods in the context of the ESPRIT DeVa (Design for Validation) project. The principles consist of a theory, a methodology and a tool for the selection of tests from a CO-OPN specification and finally the execution of such tests on concurrent programs.
System Validation
In order to support a part of the validation process, we propose a way of using the analysis phase of the Fusion Method developed by Hewlett-Packard as a first step in describing system requirements. Then, we give guidelines for the semi-automatic transformation of the Fusion specification document into a CO-OPN formal specification. Of course this approach does not allow the validation of all the system requirements and must be coupled with traditional validations activities.
For more information on CO-OPN, see http://lglwww.epfl.ch/~coopn
Please contact:
Didier Buchs - Swiss Federal Institute of Technology
Tel: +41 21 6932737
E-mail: Didier.Buchs@di.epfl.ch