Medium/Large examples in Lustre

## Medium/Large examples in Lustre

subway
An subway system, parameterized by the number of different trains on the same track, coming from [6]. This example is extracted from an actual proposal for an automatic subway. It concerns a (simplified version of a) speed regulation system avoiding collision. Each train detects beacons that are placed along the track, and receives the "second" from a central clock. Ideally, a train should encounter one beacon each second. So the space left between beacons rules the speed of the train. Now, a train adjusts its speed as follows: let #b and #s be respectively the number of encountered beacons and the number of received seconds.
• When #b >= #s + 10, the train notices it is early, and puts on the brake as long as #b > #s. Continuously braking makes the train stop before encountering 10 beacons (using a counter c).
• When #b <= #s -10, the train is late, and will be considered late as long as #b < #s. A late train signals it to the central clock, which does not emit the "second" as long as at least one train is late.

The picture aboved shows the automaton for one subway, after removing the unfeasible transitions. The transition functions of #b and #s are not displayed, and the guards are given using primed variables (substituting to them their transition functions leads to more tricky conditions). This system does not exhibit many Boolean variables, and actually the classical technique of [6] performs well. We aim, here, at showing that our refinement heuristic is powerful enough to separate relevant states to prove properties without introducing too many locations. We wish to prove the following properties, on a system with n trains sharing the central clock
1. A train cannot move in one step from the state late to the state on_brake, and conversely. If there are several trains, we prove it for the first one.
2. The number #b-#s remain in the interval [-10,20]. This property can be decomposed in the conjunction of
• a) #b-#s >= -10;
• b) #b-#s <= 20.
3. When there is at least two trains, their respective numbers of beacons, #b1 and #b2 satisfy #b2-#b1 <= 40. This means that if they are initially separated by 40 beacons, they will never collide.
4. Same property, but with the real bound: #b2-#b1 <= 29.
5. Symmetrical property |#b2-#b1| <= 30.
lift
A lift system, parameterized by the number N of levels, and also by the delays. The goal is to check duration properties between two events. This example exhibits complex Boolean behavior, while containing some counters, and represents a good target for our tool. The lift controller, taken,from [1], is depicted below. The lift has N floors. At each floor, there are "up" and "down" request buttons, and in the cabin N request buttons allowing a user to choose the destination floor. The requests are buffered, which results in a quite complex control. The controller has also to set information lights adequately. Concerning the cabin, opening and closing the door are modelled, as well as its moves, decomposed by half floors for the departure and the arrival.

We have modified the original program by adding counters to model the time taken by the lift to move up or down (from one floor, or half a floor for departure and arrival), and the time needed by the door to be opened or closed. Most logical properties can be proved on this system with a model checker such as LESAR [11] by considering its Boolean abstraction (case of property 1). We concentrated thus mainly on the following time properties:
1. At most one of this state is possible at a time: opening a door, closing a door, going up, going down.
2. Lower bound for the delay between closing of the doors at floor 0 and opening at floor 1.
3. Idem as the last one, but with the real bound.
4. Lower bound between two departures of the cabin from the first floor. This implies that in between, the cabin went up then down.
5. Idem as the last one, but the first floor is replaced by the second one, from which the cabin can go first up or down.
The size of the LUSTRE program with these properties is about 700 lines, with N varying from 3 to 6. The number of Boolean state variables is several dozens, and there are several input variables.

Bertrand Jeannet, February 10, 2011

 Medium/Large examples in Lustre