| Organisation: |
Université de Nantes (FRANCE)
|
| Functionality: |
Model checking for component-based systems.
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
|
| Period: |
2008 - 2010
|
| Description: |
The modelling of various real life systems (e.g., auction systems,
chat systems, distributed brokers, etc.) requires the use of several
components of the same type or several services with identical
functionalities but coming from different components. The design of
such systems needs the ability to describe the assembly and the
composition w.r.t. the multiplicity of services that may be connected.
The Kmelia abstract component model was introduced to support the
specification and development of correct components. The model is
equipped with a language allowing the description of components and
services. Two different semantics are defined for linking component
services: monadic semantics (only one provided service may be
associated to a requested service) and polyadic semantics
(a provided service may be linked with various required services).
Kmelia allows to define components and assemblies (sets of components
linked through their services). A Kmelia abstract component is a
mathematical model of an open multiservice system that supports
synchronous communication with its environment. The polyadic semantics
is defined by means of shared services and multipart communications.
Well-formed Kmelia specifications must satisfy the properties of
composability and behavioural compatibility.
Formal analysis for Kmelia is supported by the COSTO toolbox, which
is able to parse Kmelia specifications, translate them into LOTOS,
and check service properties (including behavioural compatibility)
using CADP. The negotiated multiway rendezvous of LOTOS is useful
for modelling the multipart communications between Kmelia components.
The usage of Kmelia and COSTO is illustrated on a chat system with
shared services.
|
| Conclusions: |
Process algebraic languages like LOTOS are naturally adapted to the
description of concurrency, and can serve as target languages for
translating component-based description languages like Kmelia.
A direct benefit of such translations is the direct access to the
formal analysis functionalities provided by tools like CADP. Further
work on Kmelia includes the study of sharing and related properties,
composition and correctness of component assemblies, and also the
suport for interoperability with other component models.
|
| Publications: |
[Andre-Ardourel-Attiogbe-08]
Pascal André, Gilles Ardourel, Christian Attiogbé.
"Composing Components with Shared Services in the Kmelia Model".
In Cesare Pautasso and Eric Tanter, editors, Proceedings of the
7th International Symposium on Software Composition SC'2008 (Budapest,
Hungary), Lecture Notes in Computer Science, volume 4954,
pp. 125-140, March 2008.
Full version available from the VASY FTP site in
PDF 
or
PostScript 
[Andre-Ardourel-Attiogbe-Lanoix-10]
Pascal André, Gilles Ardourel, Christian Attiogbé and
Arnoud Lanoix.
"Using Assertions to Enhance the Correctness of Kmelia Components and
their Assemblies". In Electronic Notes in Theoretical Computer
Science 263 (2010) 5-30.
Available on line from http://hal.archives-ouvertes.fr/hal-00423672/en/
or from the VASY FTP site at
PDF
or
PostScript
|
| Contact: |
Pascal André
LINA
2, rue de la Houssinière
B.P. 92208
44072 Nantes Cedex 03
France
Tel: 02 51 12 59 65
Fax: 02 51 12 58 12
Email: Pascal.Andre@univ-nantes.fr
|
| Further remarks: |
This tool, amongst others, is described on the CADP Web Page:
http://cadp.inria.fr
|
Back to the CADP research tools page