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
