TURTLE

TURTLE is now deprecated, and we encourage all users to switch to AVATAR.

TURTLE targets the modeling and formal verification of real-time embedded systems. TURTLE supports many advanced features, including a push-button approach for formal verification purpose, the automatic synthesis of a first design from analysis diagrams, and the automatic middleware code generationfrom deployment diagram. TURTLE also supports modeling patterns for protocols.

The TURTLE profile reuses both UML and SysML diagrams. TURTLE supports the following methodological phases:

1. Requirement capture. Requirements and properties are structured using AVATAR Requirement Diagrams. At this step, properties are just defined with a specific label.


2. System analysis (also called TURTLE Analysis). A system may be analyzed using usual UML diagrams, such as Use Case Diagrams, Interaction Overview Diagrams and Sequence Diagrams. Formal verification can be performed from analysis diagrams, using RTL, CADP or UPPAAL.


3. System design (also called TURTLE Design. The system is designed in terms of communicating UML classes, and in terms of behaviors described with TURTLE Activity Diagrams. Formal verification can be performed from design diagrams, using RTL, CADP or UPPAAL.


4. Deployment (also called TURTLE Deployment) can finally be conducted. It consists in mapping classes of the design on execution nodes. From a deployment diagram, formal verification can be conducted (RTL, CADP, UPPAAL), and middleware-based prototyping code can be generated.

---

Resources

Technical papers

• Paper on requirements. Published at Industrial Embedded Systems, 2006.


• Paper on TURTLE Analysis. Published at Colloque Francophone sur l'Ingénierie des Protocoles, 2005. (in French).


• Paper on TURTLE Designs . Published in IEEE Transactions on Software Engineering, 2004.


• Paper on TURTLE Deployment. Published in the Annals of Telecommunication, 2006. (in French).

Presentations

• Slides presented at UMLFM'2010


• Presentation on AVATAR given at the SysML Days, Paris, the 6th of December, 2010 (in French)

Tutorial

• Four weddings and a tutorial: explanations on the various TURTLE methodological phases, with a case study. Published at ERTSS'2010. Presented slides


• This presentation on the TURTLE methodology shall help you to start with TURTLE


• A step-by-step training:
1. Step 1: Learning UML


2. Step 2: TURTLE


3. Step 3: Using TTool / TURTLE

Examples of TURTLE models

• Coffee machine modeled with TURTLE (open the file with TTool)


• Web server - and its clients - system modeled with TURTLE (open the file with TTool)

---

Configuration

If you wish to:

• Make proofs from diagrams containing temporal operators, you need to install and configure RTL or UPPAAL


• Make proofs of on large models which contains no temporal operators, you need to install and configure CADP


• Manipulate reachability graphs, you need to install CADP for minimizing graphs and performing bisimulations. For visualizing graphs, you ought to install Graphviz