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
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.
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.
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.
Same property, but with the real bound: #b2-#b1 <= 29.
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:
At most one of this state is possible at a time: opening a
door, closing a door, going up, going down.
Lower bound for the delay between closing of the doors at floor 0 and opening at floor 1.
Idem as the last one, but with the real bound.
Lower bound between two departures of the cabin from the first floor. This implies that in between, the cabin went up then down.
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.
