TURTLE

TURTLE

A UML Profile for the Modeling and Formal Verification of Time-Constrained Systems

NEW: TTool can now be freely downloaded from this website. Select TTool, download section on the menu on the left.

What is TURTLE?

TURTLE stands for Timed UML and RT-LOTOS Environment

TURTLE is a UML profile dedicated to the modeling and formal validation of time-constrained systems. Indeed, if UML is now widely used, UML diagrams are ambiguous because UML operators lack formal semantics. For example, at class diagram level, an association between two UML classes has no formal meaning. Conversely, an association between two TURTLE classes is always given a formal meaning (Parallel, Synchronization, Sequence, etc.) at modeling step.

TURTLE adresses several methodological steps:

Requirement capture
System analysis
System design
System deployment

Thus, TURTLE defines a set of operators and diagrams adressing the need for analysing, designing and deploying temporally constrained systems. The strength of TURTLE relies in its formally semantics given in RT-LOTOS, via translation algorithms. RT-LOTOS is a Formal Description Technique, based on process algebra, and introduced at LAAS/CNRS, Toulouse, France. It is supported by a tool – RTL – with formal validation capabilities.

TURTLE has been defined with three keypoints in mind:

The use of formal language is totally hidden to TURTLE modelers. Supported formal languages are RT-LOTOS, LOTOS and UPPAAL
Executable Java code may be generated from all diagrams.
TURTLE is supported by an open-source toolkit (TTool)

The formal semantics of TURTLE makes it possible to perform formal validation directly from UML models, without any knowledge about underlying formal languages (e.g. RT-LOTOS). By formal validation, we mean either making intensive simulations, or building the minimal reachability graph of the system under design. Also, a set of tools and techniques makes it possible to analyze possible errors of the system (deadlock, etc.) and correct UML diagrams accordingly.

The first version of TURTLE – named “native TURTLE” - has been extended with several extensions dedicated to real-time systems, to protocols, and to distributed systems.

Also, a toolkit – named TTool for TURTLE Toolkit - has been implemented. It allows the edition and validation of TURTLE diagrams, as well as the analysis of simulation and validation results.

A Few Words on TTool

TTool stands for TURTLE Toolkit

TTool offers many functionalities such as edition of TURTLE diagrams, formal proofs on TURTLE diagrams, and generation of Java code from TURTLE diagrams. And TTool is free!!! (open-source software).