# Labs

You first need to install TTool 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 2020: 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**.

### Lab #1. Pressure controller and Railroad crossing 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.
- Once you have finished working with the PressureController model, you should make in TTool
**the design of the railroad crossing system system**. Once finished, you must prove the three following properties: - After an "approach", there is always at least one "in" and one "leave"
- if a train is between "approach" and "in" then either the barrier is being closed, or it is closed, or the headquarter has been informed of the problem.
- There exists at least one execution path where the barriers can receive an close order while they are opening.

### Lab #2

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

### Lab #3

- Modeling a Glucose Monitoring System (Eurecom exam of Fall 2019).
**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 2020: 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

- 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
- 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.
- Generate the Reachability Graph of this system, and minimize it to 4 actions of your choice different from the ones of the slides
- 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.

- Understand the system by reading its specification and the analysis of this system given in this TTool model.

### 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:
- 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.

### Lab #3

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