Database of Research Tools Developed Using CADP

IDCM Tool for Incremental Component-based Architectures

Organisation: Ecole des Mines d'Alès / LGI2P, Nîmes (FRANCE)
University of Montpellier (FRANCE)

Functionality: Incremental development of software architectures.

Tools used: CADP (Construction and Analysis of Distributed Processes)

Period: 2010-2012

Description: The construction of critical reactive software architectures, in which errors could have serious consequences on human life, environments or significant assets, is challenging. When constructing such architectures, one focuses on behavioral analysis in order to detect communication problems such as deadlocks between components. Hence, two aspects are considered: construction processes of architectures and evaluation techniques. The construction of architectures is supported by an incremental approach consisting of the following operations: addition (adding a component or a connection into the architecture), removal (removing a component or a connection from the architecture), substitution (substituting a component by a new one), split (separate a component into subcomponents), and merge (fusion of several components into a single one). As regards evaluation techniques, the approach adopted relies upon a transformation of UML architectures into formal models (namely, labeled transition systems, LTSs), and a comparison of the models using preorders and equivalences to ensure that a model preserves the necessary properties of the previous version.

The semantics of primitive components is determined by transforming a subset of UML state machines and activities, described using the TopCased framework, into LTSs. The semantics of architectures is defined by transforming UML composite structures into EXP.OPEN specifications by a set of rules. Then, the corresponding LTSs are generated by using the CADP toolbox. These operations have been integrated into the IDCM (Incremental Development of Conforming Model) tool. Besides generating the LTS models, IDCM provides two kinds of analyses: deadlock detection and component substitutability based on the should-testing preorder. The modeling and analysis approach is illustrated on the example of a task manager.

Conclusions: The conformance relations implemented in IDCM enable the designer to compare two models obtained during an incremental construction process. Several development methods are possible using this approach: conventional (the specifications are developed completely before the implementation), careful (the specifications are developed partially and analyzed w.r.t. feasibility or user feedback, then the implementation is extended according to the needs), or agile (the specifications and the implementation are developed simultaneously and the implementation obtained serves as basis for the initial specification of the next version of the product).

Publications: [Luong-10] Hong-Viet Luong. "Construction Incrémentale de Spécifications de Systèmes Critiques intégrant des Procédures de Vérification". Thèse de Doctorat, Université Paul Sabatier, Toulouse, Octobre 2010.
Available on-line at:
or from our FTP site in PDF or PostScript

[Lambolais-Courbis-Luong-Phan-11] Thomas Lambolais, Anne-Lise Courbis, Hong-Viet Luong, and Thanh-Liem Phan. "Interoperability Analysis of Systems". Proceedings of the 18th IFAC World Congress (Milano, Italy), vol. 18, part 1, pages 7879-7884. IFAC, August 28-September 2, 2011.
Available on-line at:
or from our FTP site in PDF or PostScript

[Luong-Courbis-Lambolais-Phan-12] Hong-Viet Luong, Anne-Lise Courbis, Thomas Lambolais, and Thanh Liem Phan. "IDCM : un outil d'analyse de composants et d'architectures dédié à la construction incrémentale". Actes des 11èmes Journées Francophones sur les Approches Formelles dans l'Assistance au Développement de Logiciels AFADL'2012 (Grenoble, France), Janvier 2012.
Available on-line at:

[Phan-Courbis-Lambolais-Libourel-12] Thanh Liem Phan, Anne-Lise Courbis, Thomas Lambolais, and Thérèse Libourel. "Incremental Construction of Architectural Specification Supported by Behavioral Verification". Advances on Cognitive Automation at LGI2P, Research Report RR12/Lab/002, pages 27-30. Ecole des Mines d'Alès, June 2012.
Available on-line at:
or from our FTP site in PDF or PostScript

[Phan-13] Thanh-Liem Phan. "Modeling and verification techniques for incremental development of UML architectures". Doctoral Symposium at ECOOP'2013 (Montpellier, France), July 2013.
Available on-line at:
or from our FTP site in PDF or PostScript

Thomas Lambolais
Ecole des Mines d'Alès / LGI2P
Parc Scientifique G. Besse
30035 Nîmes cedex 1
Tel: +33 (0)4 66 38 70 93

Further remarks: This tool, amongst others, is described on the CADP Web site:

Last modified: Tue Feb 7 10:02:54 2017.

Back to the CADP research tools page