Installing TToolYou first need to install TTool.
Installing TTool on your own computerIf 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 computersTTool 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/makeLocalInstallThis 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:
$ cd ~/TTool_local/bin $ ./ttool.exe
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 2021: Eurecom
ReportLab #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
- 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 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.
- Analysis and design of an Automotive System (Eurecom exam of Fall 2013).
- 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
ReportLabs #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.
- Open this PressureController in TTool
- 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
- 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.
- 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:
- After an "approach", there is always an "in" and a "leave"
- if a train is between an "approach" and an "in" then either the barriers are being closed or the headquarter has been informed.
- There exists at least one execution path where the barriers can receive a close order while they are closing.
- Modeling a FortiSandbox (Eurecom exam of Fall 2018). The grading is given in the description of the work to do.