Organisation: |
Ecole des Mines d'Alès / LGI2P, Nîmes (FRANCE)
University of Montpellier (FRANCE) INSA Lyon (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: http://thesesups.ups-tlse.fr/1109/1/Luong_Hong-Viet.pdf or from the CADP Web 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: http://www.nt.ntnu.no/users/skoge/prost/proceedings/ifac11-proceedings/data/html/papers/3523.pdf or from the CADP Web 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: http://hal.archives-ouvertes.fr/hal-00756230 or from the CADP Web site in PDF or PostScript [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: http://www.lgi2p.ema.fr/~urtado/Slides/RR12_Lab_002.pdf or from the CADP Web 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: http://www.lirmm.fr/ecoop13/images/ds/8-paper-thanh%20liem%20phan.pdf or from the CADP Web site in PDF or PostScript [Lambolais-Courbis-Luong-Phan-16] Thomas Lambolais, Anne-Lise Courbis, Hong-Viet Luong, and Thanh-Liem Phan. "Designing and Integrating Complex Systems: Be Agile Through Liveness Verification and Abstraction". In Complex Systems Design and Management, pages 69-81. Springer International Publishing, 2016. Available on-line at: http://link.springer.com/chapter/10.1007/978-3-319-26109-6_5 [Lambolais-Courbis-Luong-Percebois-16] Thomas Lambolais, Anne-Lise Courbis, Hong-Viet Luong, and Christian Percebois. "IDF: A Framework for the Incremental Development and Conformance Verification of UML Active Primitive Components". Journal of Systems and Software 113:275-295, March 2016. Available on-line at: https://hal.archives-ouvertes.fr/hal-01517375 or from the CADP Web site in PDF or PostScript [Lambolais-Courbis-18] Thomas Lambolais and Anne-Lise Courbis. "Development and VErification of UML Architectures by Refinement and Extension Techniques". Proceedings of the 9th European Congress on Embedded Real Time Software and Systems (ERTS2 2018), Toulouse, France, January, 2018. Available on-line at: https://www.erts2018.org/uploads/program/ERTS_2018_paper_98.pdf or from the CADP Web site in PDF or PostScript |
Contact: | Thomas Lambolais Ecole des Mines d'Alès / LGI2P Parc Scientifique G. Besse 30035 Nîmes cedex 1 France Tel: +33 (0)4 66 38 70 93 Email: [email protected] |
Further remarks: | This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software |