|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
Institut Eurecom
|
|---|---|
| Functionality: |
Verification and Simulation of TURTLE (Real-Time UML) Diagrams
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
GraphViz RTL |
| Period: |
2004-2012
|
| Description: |
TURTLE (Timed UML and RT-LOTOS Environment) is a real-time UML
profile. The semantics of TURTLE is formally defined by a translation
into RT-LOTOS.
Formal verification and simulation of a TURTLE profile is enabled by the TTool by translating a TURTLE diagram into a RT-LOTOS specification and using RTL for the generation of its reachability graph, which can be analysed, verified and minimized using CADP. For details, see the TURTLE, TTool, and DIPLODOCUS Web pages at: http://labsoc.comelec.enst.fr/TURTLE/ http://labsoc.comelec.enst.fr/TURTLE/ttoolindex.html http://www.comelec.enst.fr/recherche/labsoc/projets/DIPLODOCUS.en |
| Conclusions: |
TTool and CADP have been used successfully for the verification of
several case-studies of embedded systems and protocols.
|
| Publications: |
[SaquiSannes-Apvrille-Lohr-Courtiat-04]
Pierre de Saqui-Sannes, Ludovic Apvrille, Christophe Lohr, and
Jean-Pierre Courtiat.
"TURTLE : un pont entre UML et RT-LOTOS". In Actes des la
conférence Approches Formelles dans l'Assistance au
Développement de Logiciels AFADL'2004, (Besançon,
FRANCE), 16-18 Juin 2004 (in French).
Available on-line from http://lifc.univ-fcomte.fr/afadl2004/textes/actes/Outils/o08.pdf or from the CADP Web site in PDF 
or
PostScript 
[Apvrille-Courtiat-Lohr-SaquiSannes-04] Ludovic Apvrille, Jean-Pierre Courtiat, Christophe Lohr, and Pierre de Saqui-Sannes. "TURTLE: A Real-Time UML Profile Supported by a Formal Validation Toolkit". IEEE Transactions on Software Engineering, vol. 30, no. 7, pp. 473-487, July 2004. Available on-line from the CADP Web site in PDF
or
PostScript
[Fontan-Mota-SaquiSannes-Villemur-07] Benjamin Fontan, Sara Mota, Pierre de Saqui-Sannes, and Thierry Villemur. "Temporal Verification in Secure Group Communication System Design". In Judie Mulholland and Octavio Nieto-Taladriz editors, Proceedings of the International Conference on Emerging Security Information, Systems and Technologies SECURWARE'2007 (Valencia, Spain), pp. 175-180, October 2007. Available on-line from the CADP Web site in PDF
or
PostScript
[Apvrille-08] Ludovic Apvrille. "TTool for DIPLODOCUS: An Environment for Design Space Exploration". In Proceedings of the 8th international conference on New technologies in distributed systems NOTERE'08 (Lyon, France pp. 1-4, June 2008. Available on-line from http://portal.acm.org/citation.cfm?id=1416729.1416764 or from the CADP Web site in PDF
or
PostScript
[Fontan-SaquiSannes-Apvrille-08] Benjamin Fontan, Pierre de Saqui-Sannes, and Ludovic Apvrille. "Synthèse d'observateurs à partir d'exigences temporelles". In 14ième conférence Langages et Modèles à Objets (LMO 2008) Montréal, Canada, March 2008. Available on-line from http://www.tsi.enst.fr/publications/enst/inproceedings-2008-7691.pdf or from the CADP Web site in PDF
or
PostScript
[SaquiSannes-Apvrille-09] Pierre de Saqui-Sannes and Ludovic Apvrille. "Making Formal Verification Amenable to Real-Time UML Practitioners". In Proceedings of the 12th European Workshop on Dependable Computing, EWDC 2009, Toulouse, France, May 2009. Available on-line from http://hal.archives-ouvertes.fr/docs/00/38/19/49/PDF/RigorousDevelopment_2.pdf or from the CADP Web site in PDF
or
PostScript
[Knorreck-Apvrille-Pacalet-10] Daniel Knorreck, Ludovic Apvrille and Renaud Pacalet. "Formal system-level design space exploration". In Proceedings of the 10th Annual International Conference on New Technologies of Distributed Systems (NOTERE), 2010, Tozeur, Tunisia. Available on line from http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5536852 or from the CADP Web site at PDF
or
PostScript
[Apvrille-12] Ludovic Apvrille. "Model-Based Design of Complex Embedded Systems". Habilitation à Diriger les Recherches, Université de Nice Sophia-Antipolis, November 2012. Available on line from http://perso.telecom-paristech.fr/~apvrille/docs/hdr_la.pdf or from the CADP Web site at PDF
or
PostScript
|
| Contact: | Ludovic Apvrille ENST, LabSoC Laboratory Institut Eurecom BP 193, 2229 Routes des Cretes 06904 Sophia-Antipolis Cedex FRANCE Tel: +33 (0)4 93 00 27 74 Fax: +33 (0)4 93 00 26 27 Email: ludovic.apvrille@enst.fr |
| Further remarks: | This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software |
Back to the CADP research tools page