Train gate example is a railway control system which controls access to a bridge for several trains. The bridge is a critical shared resource that may be accessed only by one train at a time. The system is definedas a number of trains(assume 4 for your project)and a controller.

Figure 1: A train gate example that describes the temporal constraints as well as the many states that a train can be in. The annotations in orange show the states ofa train.

Figure 1 depicts four trains on distinct lines that cross a shared bridge. Initially, the trains are adequately distant from the bridge. When a train approaches the bridge, the gate controller receives a notification 20 time units before the train arrives (approaching). The gate controller has the ability to stop, restart, or allow the train to proceed. If the train is not halted within 10 time units, it must pass the bridge. If the train is stopped (stop), it will ultimately be restarted (restart), and the trip to the bridge will take 7-15 time units. It takes 3-5 time units for a train to cross the bridge (crossing). Following the crossing, the train will return to its safe state and alert the gate controller. Note, the system must ensure that only one train at a time has access to the bridge.

One of the four trains is a specialtrain with the highest priority. This means that anytime this train arrives,the bridge must be clearedright away. Even if thereare multiple trainsin the stoppable area, the special train should have priority. If the bridge is occupied, the special trainwill come to a halt and will be given a go signal as soon as the bridgeis clear.

Every train approaching the bridge is placed in a queue. The queue maintains track of arriving trains and their arrival order. Trains are permitted to cross the bridge based on this order when numerous trains approach at the same time or immediately one after the other. Because the number of trains is fixed, i.e. 4, create a template in addition to controller and train that assures the trains arrive and depart inthe same order. Priority should be given to special trains.

Questions:

Q1. Based on the class on Uppaal demo model checking, create this model in Uppaal. Perform the model checking. (15 Marks)

Q2. In class we discussed the IoT design methodology. Continuing the philosophy, design a prototype set up for the train-gate example. You may need to collect the information on sensors and actuators based on the constraints, for example in this case proximity sensor. Design the process model, domain model, deployment model and operational view model. (10 Marks)

Suggestions and Tips:

1. The answer to the question may vary based on your assumptions. Hence make your assumption explicitat beginning.
2. Justify your modeling choices.
3. For Uppaal modelling, I will require the .xml file of the model and query file.
4. I prefer a working small model to complicated not working model
5. You may add context if needed.
6.  

Safe I 0 Stop -- Restart Approaching Stoppable Area Train is stoppable A-+-- 1 7-5 I 1 I 1 Train musti I proceed I 10 27 Crossing 3-5 Safe 1 Time