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 11 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). Alternatively, 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/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:

~/myTTool/ttool.exe

or:

$ cd ~/myTTool/
$ ./ttool.exe

Note: exams are done on Eurecom computers. You will have to test your installation of TTool on Eurecom desktops before the exam.

How to start?

Then, two videos could help you starting with TTool:

My first Avatar model (video): how to make an AVATAR design, and how to perform simulations.

Safety verification of Avatar models (video): how to perform formal safety verifications from Avatar / TTool models

You may also consult the tutorial on AVATAR

Fall 2025: Eurecom

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 Software of the mobile application of a bike reservation system

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.

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

Create a new model for the Software of a Smart Greenhouse Automation System. You should make the design of this software. Once finished, you must prove the three following properties:

In automatic mode, the fan is turned on whenever the temperature goes over a threshold.
A user can turn the heating system on, even if the temperature is already too high.
No temperature alerts are sent to users when if the temperature is within correct ranges.

Lab #2

Analysis and design of a bike reservation systems (Eurecom exam of Fall 2023).

Lab #3

Analysis and design of a glucose monitoring system (Eurecom exam of Fall 2019). GRADED: you have a one week delay to send me your report and model by email (ludovic.apvrille A.T. telecom-paris.fr). "until" means until the next Thursday, 13:30

Lab #4

Analysis and design of an Automotive System (Eurecom exam of Fall 2013).