DIPLODOCUS
(DesIgn sPace exLoration based on fOrmal Description teChniques, Uml and SystemC)
NEW: A short movie presenting DIPLODOCUS and TTool
The DIPLODOCUS UML profile is meant to implement features defined in the MASC project. It partially supports the methodology defined in MASC with a mixed UML / SysML approach. The DIPLODOCUS environment is supported by the TTool UML toolkit. This toolkit is free. It supports other UML profiles than DIPLODOCUS.
Hereafter, when we mention DIPLODOCUS, we mean "TTool for DIPLODOCUS".
Using TTool for DIPLODOCUS
- Installing and starting TTool for DIPLODOCUS
- Making an application modeling in UML
- Making an application modeling in textual form
- Making an architecture in UML
- Making an architecture in textual form
- Making a mapping in UML
- Making a mapping in textual form
- Formal verification (LOTOS, UPPAAL)
- Simulation (SystemC)
- Examples
Main DIPLODOCUS functionalities
- Edition of application modeling
You may either use UML diagrams or a file in TML language to describe your application in terms of communicating tasks. From that description, either in UML or in text format, you may either generate LOTOS code, UPPAAL code, or SystemC code. From a UML specification of your application, you may also generate a textual TML specification (.tml file)
- Edition of architecture and mapping
Once again, you may do this either with UML, using a deployment diagram, or in a textual form. From the UML deployment diagram, you may generate a textual representation.
- Formal verification
The purpose of formal verification is to prove that all traces of the system satisfy a given set of properties. Formal verification relies on either LOTOS or UPPAAL, generated from a (hidden) intermediate format - called TML Intermediate Format - internal to TTool. With LOTOS, it relies on CADP. The latter generates a reachability graph that can be studied afterwards, either directly from TTool or using third-party toolkits. With UPPAAL, deadlock or liveness properties may be verified directly from TTool. CTL formulae may also be captured int TTool for verification purpose.
- Simulation
SystemC code may be generate from the two TTool internal languages (that is, TML Intermediate Format and TMAP Intermediate Format). SystemC code may be generated, compiled and executed directly from TTool. Resulting waveforms may be visualized with third-party toolkits.
Main DIPLODOCUS UML modeling functionalities
Application modeling
The application is modeled using a UML class diagram, and one UML activity diagram per class. Relations between class are channels, events and requests.
The following picture depicts a basic class diagram in which two tasks are declared.
Also, the following diagram presents the activity diagram of task1.
Once you have performed the modeling of your system, you may either simulate it, or do some formal proofs using CADP or UPPAAL.
Architecture modeling
A DIPLODOCUS architecture is modeled using a UML deployment diagram. On this deployment diagrams, hardware nodes may be mapped, and the attrbiutes of the node may be set.
Requirement modeling
Currently, requirements are used only for documentation purpose. We expect to take them into account at simulation or formal verification steps in a near future.
Mapping phase
The mapping is modeled using the architecture diagram enhanced with mapping information. Tasks may be mapped over nodes using UML artifacts.
For example, on the following mapping, three tasks have been mapped on one CPU node.
Main DIPLODOCUS simulation and verification capabilities
Formal verification with LOTOS
Generating LOTOS code makes it possible to use the CADP toolkit transparently from TTool. Thus, from TTool, you may generate a reachability graph, analyze it - for example, to search for deadlock situations - perform minimizations according to selected relevant actions, and display it (using dotty).
For example, the following picture depicts the analysis of a reachability graph (smart card example) : it has more around 40kstates.
This graph has been minimized to event waiting actions of the task called InterfaceDevice, and then it has been displayed:
Formal verification with UPPAAL
UPPAAL may be used transparently from TTool. Thus, you may select a given action in your TML design, and automatically check out whether your action is reachable (that is, one path leads to it) and always reachable (i.e. all paths should go through that actions = liveness property). Other more complex properties may also be analyzed.
For example, on the next diagram, on action has been selected : the receiving of an event called data_Ready_SC in the InterfaceDevice class of th smart card example.
Then, using the UPPAAL model checker transparently, TTool has informed the modeler that is action satisfies the reachability property, but not the liveness property (see next figure).
Simulation with SystemC
The SystemC simulation is intended to be used to produce one possible trace of the modeled system. A set of SystemC classes are first generated from DIPLODOCUS diagrams. Then, they are compiled and linked to SystemC libraries we provide. At last, the produced executable file is executed, and the simulation results are produced (in a vcd file). They may be displayed using gtkwave, for example (see the following figure).
