Course on UML for Embedded Systems - Fall 2024
Main Info Schedule Documents Labs Exams Links
UMLEmb
UML
for
Embedded
Systems

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). Alternatevely, 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/bin
$ ./ttool.exe



How to start?

Then, two videos could help you starting with TTool:

You may also consult the tutorial on AVATAR


Fall 2024: 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

  1. 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.

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

  3. Create a new model for the Software of the mobile application of a bike reservation system. You should make the design of the bike reservation system. Once finished, you must prove the three following properties:
    • A ride never starts without an unlock of the bike
    • A ride always results in a lock a the bike, apart if an incident is sent to the control center
    • A reservation is always freed after 5mn or used

Lab #2

Lab #3

  • Analysis and design of a space-based embedded system (Eurecom exam of Fall 2021). 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 Friday, 13:30

Lab #4





Fall 2023: 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. I don't expect a report for the other labs.

Lab #1. Pressure controller and space-based embedded system

  1. 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.

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

  3. Create a new model for the Space-based embedded system. You should make the design of the platooning system. Once finished, you must prove the three following properties:
    • A TC always results in a TM, apart if another TC is received before sending the TM.
    • A cancelled TM is never sent.
    • When a task crashes, the watchdog restarts the system at most 10ms after it has crashed.

Lab #2

Lab #3

  • Modeling a Digital augmented hand cart (Eurecom exam of Fall 2022). 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 tuesday, 13:30

Lab #4





Fall 2023: Polytech Nice

Report

Lab #2 and lab#3 are graded (30% of your final grade).

Lab #1. Pressure controller and salmon packing system

  1. 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.

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

  3. You should make the design of the salmon packing system. Once finished, you must prove the three following properties:
    • At most one salmon is put in a container.
    • A salmon is never put on the conveyor if no container is present.
    • If a salmon and a container is present, the arm puts the salmon in the container in less than 10 units of time

Lab #2

  • Modeling a Space-based system. GRADED: you have to send your report and model by email (jawher.jerray A.T. telecom-paris.fr) before October 12 at 12:00 p.m.

Lab #3

  • Modeling a Glucose monitoring system. GRADED: you have to send your report and model to jawher.jerray A.T. telecom-paris.fr before October 19 at 4:30 p.m.






Fall 2022: 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. I don't expect a report for the other labs.

Lab #1. Pressure controller and platooning system

  1. 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.

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

  3. Create a new model for the Platooning System. You should make the design of the platooning system. Once finished, you must prove the three following properties:
    • A distance below min always result in an emergency braking in all vehicles of the platoon.
    • No new vehicle can join the platoon without a join message.
    • When a new follower joins, it is always added at the last position of the platoon.

Lab #2

Lab #3

  • Modeling a Space-based system (Eurecom exam of Fall 2021). 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.

Lab #4





Fall 2021: 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

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

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:
    1. After an "approach", there is always an "in" and a "leave"
    2. if a train is between an "approach" and an "in" then either the barriers are being closed or the headquarter has been informed.
    3. 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.




(c) L. Apvrille, Telecom Paris
Invisible border