# Tp of Timed Automata (TA) ta modeling and Verification Goals

View original pdf
 Date 14.11.2023 Size 132.68 Kb. #62595
TP Train sujet

TP of Timed Automata (TA)
TA Modeling and Verification
Goals:
In this TP, we will model a simplified train crossing system, for which it is essential that on detecting the approach of a train, the gate should be closed within a certain time bound in order to halt car and pedestrian traffic before the train reaches the crossing.
1
One Train
Now consider the simplest situation there is only one train that will cross the gate with the help of the control system but it can cross the gate many times. For this train crossing a control system needs to be developed that closes the gate on detecting a signal indicating that the train is approaching and only opens the gate once the train has signaled that it entirely crossed the road. The safety property that should be established by this system is that the gate is always closed when the train is crossing the road. The complete system consists of the three components:
Train, Gate, and Controller.
Exercise 1 : Modeling
Now the descriptions of the three components are given as follows. For each component, please propose a TA
with one local clock to represent its behaviors corresponding to its description Train it has three states (far, near, cross). When the train is in the initial far state, it can send a signal
appro to the controller when it is near to the crossing, and thus enter the near state, where its maximum stay is 5 time units (<= 5) and the minimum stay is 2 time units (>= 2). Then the train goes to the cross
state, from where the train has to exit the crossing section by sending the signal quit to the controller at maximum 5 time units (<= 5) after sending the signal appro.
• Gate there are four states (open, down, closeup i) for the TA representing the behaviors of the gate. The gate can receive the signal lower from the controller when it is in the initial open state to pass to the down
state, where it can stay at maximum 1 unit time before entering the close state. The gate may then receive the signal raise from the controller when it is in the close state to pass to the up state, where its maximum stay is 2 time units and its minimum stay is 1 time unit, before returning back to the initial open state.
• Controller this subsystem is to control the crossing system with four states (idle, to_lower, wait, to_raise),
among which the idle state is the initial one, where the controller can receive the signal appro to know that the train is approaching the crossing. Then it enters the to_lower state, where its stay is exactly 1 time unit,
and then sends the signal lower to the gate before entering the wait state. The controller receives the signal
quit from the train when it is in the wait state to go to the to_raise state, where it can stay at maximum time unit before sending the signal raise and going back to the initial idle state.
Exercise 2 : Verification
Once you have the model of the crossing system composed of the three TAs, please check the following properties by using UPPAAL verifier:
1. the approaching train will certainly pass the crossing. the train can be in the cross state only when the gate is closed. the system is deadlock-free.
If your TAs respect the above description, the second safety property does not hold. Please understand and find out the problem before modifying a guard condition in the Train such that this property becomes true.
2
Two trains
Now please model the same crossing system with two trains. The file access system you have seen during the TDs can inspire you to model this system.
CentraleSupélec 2023-2024
1/ 2

TP of Timed Automata (TA)
Exercise 3 : Modeling
Here are some useful instructions add a Boolean variable blockade, whose value true represents that one train is currently crossing the road.
Precisely, each time when a train is approaching the crossing, then the value of blockade is modified from false to true add one state stop in the TA modelling the train, that can be reached from the state far only when the variable blockade is true for the whole system, before going back to the initial state, one should handle two situations differently:
whether the other train is waiting for the crossing in the stop state or not. If the other train is in the stop
state, please think about the right place about how to receive and emit anew channel release_wait to release the other train from the state stop. To make sure that the other train will not wait infinitely, you can add commit state after the state stop such that once this other train is released from the stop state, it can immediately obtain the access to the crossing. Furthermore, to distinguish whether there does exist awaiting train or not, a global Boolean variable wait can be added.
Exercise 4 : Verification
Besides checking all the properties described for the one train case, please also check the following properties by using UPPAAL verifier:
1. It is impossible that the two trains cross the road at the same time. Await train (in the stop state) will certainly pass the crossing. Any train may in the stop state.
If any of the above properties is false, please modify your model such that all of them are true.
CentraleSupélec 2023-2024
2/ 2

• One Train
• Two trains