LabsYou 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
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.
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.
- Analysis and design of an Automotive System (Eurecom exam of Fall 2013).
- 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
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.