UMLEmb
UML
for
Embedded
Systems

Labs

Installing TTool

You first need to install TTool.

Installing TTool on your own computer

If you want to use TTool on your own laptop, then, you need to download it and then to install it. Select the development version, graphical installer. You need to have Java 8 at least installed on your computer.
Once downloaded, just uncompress the file, go in the TTool directory, and start it with ttool.bat (windows) or ttool.exe (MacOS, Linux). Alternatevely, in Windows, you can simply double click on ttool.jar in TTool/bin directory

Using TTool on Eurecom computers

TTool packages are installed in /opt/ttool/
To be able to use TTool, you first need to install the configuration of TTool in your home directory. To do so, execute from a terminal the following command:
$ /opt/ttool/local_install/makeLocalInstall
This should create a directory named TTool_local in your home directory. This is done once for all, you don't need to re-execute that script in the future, apart when TTool is updated (your favourite teacher will tell you when to do this again if necessary).

Now, to start TTool, do as follows:
~/TTool_local/bin/ttool.exe
or:
$ cd ~/TTool_local/bin
$ ./ttool.exe



How to start?

Then, two videos could help you starting with TTool:

You may also consult the tutorial on AVATAR



Fall 2021: Eurecom

Report

Lab #3 is graded (30% of your final grade). You have a one week delay to send me your report and your model(s) after lab #3. I don't expect a report for the other labs.

Lab #1. Pressure controller and glucose monitoring system

  1. Use the Pressure controller model. Propose two safety pragmas significantly different from the ones in the slides, one dealing with states and the other one with attributes. One pragma must be satisfied, and the other one must be non satisfied. Verify the pragmas..

  2. Generate the Reachability Graph of this system, and minimize it to 4 actions of your choice different from the ones of the slides.

  3. Create a new model for the Glucose Monitoring System. You should capture in TTool your sequence diagrams of the Glucose monitoring system (to create a sequence diagram: right click in the main panel, "new Analysis". Then another right click, "new Sequence Diagram"), and then you should make the design of the glucose monitoring system. Once finished, you must prove the three following properties:
    • Whenever a new glycemia value is available in the sensor and there is an active connection between the sensor and the mobile application, then the glycemia value is updated in the mobile application within one minute (i.e. before a new glycemia value is available in the sensor).
    • No glycemia value sent by the sensor shall be saved nor displayed in the mobile application once the sensor is supposed to have expired.
    • Getting no glycemia value means that either the sensor has not yet been activated or it has expired, or the connection between the sensor and the mobile app is not established.

Lab #2

Lab #3

  • Modeling a Platooning System (Eurecom exam of Fall 2020). GRADED: you have until the exam to send me your report and model by email (ludovic.apvrille A.T. telecom-paris.fr). "until" means before the beginning of the exam.




Fall 2021: Polytech'Nice

Report

Labs #2 and #3 are graded. You must send a report and the models for labs #2 and #3 maximum one week after the last lab. Labs should be sent by email to your lab supervisor.

Lab #1

  1. Open this PressureController in TTool

  2. Perform simulations of the model. Using the simulator, make the following traces:
    • Start the alarm
    • Start the alarm, and then see what happens when a second "highPressure" is detected while the alarm is already "ON"
    • Show a trace when the alarm has been set to "ON" and then to "OFF"
    • Show a (long) trace where the alarm is never started
  3. Propose two safety pragmas different from the ones in the slides. One pragma must be satisfied, and the other one must be non satisfied. Verify the pragmas using UPPAAL.

  4. Generate the Reachability Graph of this system, and minimize it to 4 actions of your choice different from the ones of the slides

  5. Once you have finished working with the PressureController model, you should make in TTool the design of the FAN1 system (specification provided by Airbus).
    • Understand the system by reading its specification and the analysis of this system given in this TTool model.
    • Perform the design of this system for an unlossy communication network.
    • Now, assume the communication network can lost CC messages. Update your design, and simulate to verify that the message can be lost or not, and that the pilot is informed in both cases. Prove this property with a pragma.

Lab #2

  • Design of the Railroad crossing system. 12 points are given for the quality of your design. 8 points are given for the verification. Check that:
    1. After an "approach", there is always an "in" and a "leave"
    2. if a train is between an "approach" and an "in" then either the barriers are being closed or the headquarter has been informed.
    3. There exists at least one execution path where the barriers can receive a close order while they are closing.

Lab #3

  • Modeling a FortiSandbox (Eurecom exam of Fall 2018). The grading is given in the description of the work to do.