UMLEmb
UML
for
Embedded
Systems

Labs

Two videos could help you starting with TTool:

If you want to use TTool on your own laptop, then, you need to download it and then to install it. Fully pre-installed version for Windows/MacOS/Linux are also available, but beware: you have to have a valid authorization to use UPPAAL Once downloaded, just uncompress the file, go in the TTool directory, and start it with ttool.bat (windows) or ttool.exe (MacOS, Linux).


Fall 2018: Eurecom

Installing TTool

TTool packages are installed in /packages/LabSoC/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:
$ /packages/LabSoC/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).
Now, to start TTool, do as follows:
~/TTool_local/bin/ttool.exe
or:
$ cd ~/TTool_local/bin
$ ttool.exe


Report

Labs are graded (30%). You should provice a report and the models for labs #2 and #3 before the day of the exam.

Lab #1

  1. Open the PressureController model 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 Railroad crossing system. Once finished, you must prove these two properties:
    • When a train enters the crossing, either a message is sent to the HQ or the barriers are lowered
    • Two trains can be at the same time between "approach" and "leave"

Lab #2

Lab #3

  • Modeling a Rover (Eurecom exam of Fall 2017).




Fall 2018: Polytech'Nice

Installing TTool

A fully pre-installed version for Linux is available there. Just uncompress it, go in the TTool/Linux directory, and start it with ttool.exe

Report

Labs #2 and #3 are graded. You should provice a report and the models for labs #2 and #3 before the day of the exam.

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 Drone system. Once finished, you must prove these two properties:
    • A drone will eventually land
    • A drone will make an emergency land when the WIFI system fails and while the drone is following a path

Lab #2

Lab #3

  • Modeling a Rover (Eurecom exam of Fall 2017).