Database of Research Tools Developed Using CADP

TTool (TURTLE Toolkit)

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 our FTP 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 our FTP 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 our FTP 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 our FTP 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 our FTP 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 our FTP 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 our FTP 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 our FTP 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


Last modified: Fri Feb 19 09:13:01 2016.


Back to the CADP research tools page