IMITATOR

Tutorial on IMITATOR

Practical information in a nutshell

The tutorial took place in July 2024 at VTSA 2024 (Luxembourg).

0) Download IMITATOR

The version used for this practical session is IMITATOR 3.4.0-alpha "Cheese Durian".

The user manual is available there: IMITATOR-user-manual.pdf.

1) Verification of a railway crossing system

railway crossing system

Let us consider a railway crossing system with the following specification.

This railway crossing consists in a track crossing a road. Trains can only run in one direction, on a single track. Only one train is present in the system at a time.

A sensor is installed on the tracks, at some distance prior to the railway crossing. The parametric time between the date when the train enables the sensor (action approach) and the date when it reaches the crossing (action pass) is dApproach. When the train enables the sensor, this triggers the start of the gate going down (action startDown). The parametric time between the date when the train enables the sensor and the date when the gate starts to lower is dStartDown. The parametric time between the date when the gate starts lowering and the date when the gate is entirely down (action endDown) is dGetDown.

To keep the system simple, we assume that, if the train has passed when the gate was completely down, then the system restarts in its initial state immediately (i.e., the gate goes back up instantaneously and the train leaves immediately the crossing).

We suppose that cars, bicycles or pedestrians may still cross while the gate is not entirely closed. If the train passes while the gate is not entirely closed, then a collision occurs (technically, may occur), and the system ends in a special location crash.

The goal will of course be to synthesize parameter valuations for dApproach, dStartDown and dGetDown guaranteeing the system safety.

  1. Download and open the file train.imi using your favorite text editor (if you use a KDE environment, Kate with the Ocaml highlighting mode does an almost-perfect job)
  2. Generate a graphical version of the model as follows: 
    ./imitator train.imi -imi2PNG
    This will generate a file train-pta.png
  3. Understand the system, and guess what is the role of each location, by rereading the system description above
  4. What is the location that should be unreachable?
  5. Create a property file train.imiprop, and input the property that should be verified. The syntax is as follows: 
    property := #synth AGnot(loc[system] = SOMETHING);
    (where SOMETHING should be replaced with the name of the location that shall not be reachable)
  6. Run IMITATOR to automatically synthesize the parameter valuations for which the system is safe: 
    ./imitator train.imi train.imiprop draw-statespace full
  7. IMITATOR will output the result on screen (below "Final positive constraint guaranteeing global safety"). What are the parameter valuations guaranteeing the safety of this railway crossing system?
  8. Open the file train-statespace.pdf (that has been automatically generated by IMITATOR); what is this?

2) Specification and verification of a coffee machine

Espresso machine

Let us now write a model for a coffee machine frequently used in the presentations describing IMITATOR.

  1. Download and open the skeleton model coffee.imi using your favorite text editor
  2. Enter the following coffee machine model
    Coffee machine
    (you may want to reuse the syntax from the previous train.imi file)
    You are advised to frequently use the -imi2PNG command to visualize graphically your automaton and check the syntax.
  3. Using the appropriate command and the appropriate property, synthesize parameter valuations for which it is impossible to get a coffee.
    What constraint do you obtain? Can you explain it?

3) A distributed system

  1. Download and open the file distributedRTS.imi using your favorite text editor (if you use a KDE environment, Kate with the Ocaml highlighting mode does an almost-perfect job)
  2. Generate a graphical version of the model as follows: 
    > ./imitator distributedRTS.imi -imi2PNG
    This will generate a file distributedRTS-pta.png This model is non-parametric. Which real-time system is this model modeling? How many tasks? How many processors? Which tasks are triggered by other tasks? Are periodic? Are sporadic?
  3. Open the property file distributedRTS.imiprop. What is the safety property?
  4. Schedulability reduces here to safety checking. Perform schedulability analysis using the following command: 
    > ./imitator distributedRTS.imi distributedRTS.imiprop
    The system is schedulable if and only if the answer of safety is "true", i.e., no deadline miss is reachable.
  5. Let us now parameterize the WCET of Task 1.1. This is achieved by commenting the value of parameter WCET_T11 ("= 5") in the header. The resulting file can be obtained here. Parametric schedulability reduces to parametric safety checking. Perform parametric schedulability analysis using the following command: 
    > ./imitator distributedRTS-1-WCET11.imi distributedRTS.imiprop
    The system is schedulable for exactly the set of valuations output by IMITATOR.
  6. Let us now parameterize the WCET of both tasks 1.1 and 2.1. This is achieved by commenting the value of parameters WCET_T11 and WCET_T21 in the header. The resulting file can be obtained here. Parametric schedulability reduces to parametric safety checking. Perform parametric schedulability analysis using the following command: 
    > ./imitator distributedRTS-2-WCET11-21.imi distributedRTS.imiprop -draw-cart
    The system is schedulable for exactly the set of valuations output by IMITATOR. The generated file distributedRTS-2-WCET11-21_cart.png shows a graphical representation of the schedulable parameter space.
  7. Let us now parameterize (only) the offset of Task 2.1. This is achieved by commenting the value of parameter offsetT21 in the header. The resulting file can be obtained here. Parametric schedulability reduces to parametric safety checking. Perform parametric schedulability analysis using the following command: 
    > ./imitator distributedRTS-3-offset21.imi distributedRTS.imiprop
    The system is schedulable for exactly the set of valuations output by IMITATOR.
  8. Let us now parameterize the WCET of both tasks 2.1 and 2.2. This is achieved by commenting the value of parameters WCET_T11 and WCET_T21 in the header. The resulting file can be obtained here. Parametric schedulability reduces to parametric safety checking. Perform parametric schedulability analysis using the following command: 
    > ./imitator distributedRTS-4-WCET21-22.imi distributedRTS.imiprop -draw-cart
    The system is schedulable for exactly the set of valuations output by IMITATOR. The generated file distributedRTS-2-WCET11-21_cart.png shows a graphical representation of the schedulable parameter space.

4) Additional exercise: A history of noodles

After a long and tiring day working on real-time systems at ETR 2017, a scientist comes back home to cook noodles. S/he puts a pot on a cooking stove at t = 0. After some arbitrary time, s/he starts a timer (action start). The timer will ring pTimer seconds after start (action ring).

At t = pBoilOver, if the timer has not rung yet, the pot boils over (action boilOver). However, if the timer rung before t = pBoilOver, then the pot does not boil over, and noodles are ready! (action ready)

  1. By getting help from the syntax of the previous models, build an IMITATOR input file noodles.imi modeling the noodles problem described above. This PTA will:
    • contain at most 2 clocks;
    • only contain the actions mentioned in the problem description;
    • only contain the two parameters pTimer and pBoilOver;
    • only contain guards and invariants in the form x ~ p, where x is a clock, p a parameter, and ~ a comparison operator in {<, <=, = , >= , >}.
  2. What are the parameter valuations guaranteeing that the pot never boils over? Is this result surprising? Please explain.

Bibliography

[AHV93]
Rajeev Alur, Thomas A. Henzinger, Moshe Y. Vardi: Parametric real-time reasoning. STOC 1993: 592-601.
[Andre21]
Étienne André. IMITATOR 3: Synthesis of timing parameters beyond decidability. In Rustan Leino and Alexandra Silva (eds.), CAV’21, Springer LNCS 12759, pages 1-14, July 2021. DOI: 10.1007/978-3-030-81685-8_26 Creative Commons Attribution 3.0 Unported (CC BY 3.0) (English) [data | Slides]🌐
[LSAF14]
Giuseppe Lipari, Sun Youcheng, Étienne André and Laurent Fribourg. Toward Parametric Timed Interfaces for Real-Time Components. In Étienne André and Goran Frehse (eds.), SynCoP’14, EPTCS, April 2014.