TURTLE



TURTLE targets the modeling and formal verification of real-time embedded systems. TURTLE supports many advanced features, including a push-button approahc 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

Presentations

  • Slides presented at UMLFM'2010

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

Tutorial

Examples of TURTLE models



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