|
|
The
SMV (Modélisation
et Vérification de Logicel/Software Modelling and Verification)
group is involved in several projects directed towards the development of methods,
techniques and tools for the formal construction of large, complex and
reliable distributed systems. It is well accepted that the development
of large and complex systems needs appropriate methods. The use of formal
techniques as well as supporting tools are key for managing their inherent
complexity. This project proposes a formal specification language called
CO-OPN:
Concurrent Object Oriented Petri Nets. Behavioural concurrency aspects
are supported by algebraic nets while data-structures are modelled by algebraic
abstract data types. Tools have been built to support this formalism and
are namely a graphical editor, a compiler, and a simulator for prototyping
specifications. This environment, called CoopnBuilder, is freely available.
Task 1: System modelling
We propose to study new concepts of object orientation, such as observational
subtyping and another modelling dimension, namely timing notions, that
we want to introduce in the CO-OPN specification language. We are also
interested in the development of a set of primitives reducing the complexity
of the process of subtype validation.
-
People involved : David Hurzeler, Sandro Costa, Didier Buchs
-
Selected list of publications [1]
Task 2: 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. The abstract semantics of
CO-OPN introduce high-level synchronization concepts that is necessary
to implement by means of complex algorithms.
Task 3: System verification
We developed formal testing methods in the context of the DeVa project.
The principles used 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.
Task 4: Development of supporting tools
We are continuing to develop the CoopnBuilder environment.
Task 5: Experiment on real problems
Task 5.1: Mobile Computing
We are exploring the semantics of messengers in collaboration with the
Telecommunication group at CUI (J. Hulaas)
Task 5.1: MORM: Man machine Occupational Risk Modeling
We are developping a method for the risk evaluation in the context of industry
(MORM project).
-
People involved: A. Besrour, D. Buchs, D. Vernez (IST, Lausanne) , G. Pierrehumbert
(IST, Lausanne), D. Bauer (Winterthur)
-
Selected
list of publications
|
