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

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