Task 1: CSP and the concurrent systems (70%) A bridge over a river is only wide enough to permit a single lane of traffic. Therefore, cans can only move concurrently if they are moving in the same direction. For the simplicity of modelling, we consider all the cars moving from left to right are RED, and all from right to left are BLUE. For example, some blue cars entering the bridge are illustrated by the following diagram. UFCFYN-15-M-Analysis and Verification of Concurrent Systems 4 However, a crash can occur if two cars moving in different directions enter the bridge at the same time, which violates the safety property. A car can approach the bridge, enter and leave the bridge. Note that we dont consider any time issue in the system. For example, cars enter or leave the bridge instantaneously. In the system, there are THREE red cars and THREE blue cars, which can move concurrently. To model the system, THREE processes should be constructed at least, i.e., one process to denote the concurrent behaviour of three red cars, and one for three blue cars, and one to model the bridge to interactive with all cars. Task 1.1: (10%) Design and draw a labelled transition diagram of the bridge. The bridge should be able to interact with any car. However, it must follow one rule that the car enters the bridge firstly and leaves the bridge firstly. The one lane system does not allow the overtaking. The system can identify some bad behaviours which violate the safety property and can lead to the event crash. Note that the event crash should not interfere the behaviour of the bridge. For example, the occurrence of the event crash should not stop the system. Overall, the transition system of the bridge should satisfy three requirements: Identification of the bad behaviours to violate the safety property (no crash); Controlling of the cars with the first-in and first-out rule; No interference on cars behaviours except that it satisfies the above requirements. Task 1.2: (15%) Construct the complete system (cars and the bridge) and verify the safety property to check whether the event crash can happen. The CSP scripts for the system and the specification should be given in FDR, in which the refinement should be executed too. Task 1.3 (15%) To satisfy the safety property that no crash can happen, we introduce two signals, which are modelled as two events, to design a control system. When a car approaches the bridge, it must obtain the near-end signal first, and then obtain the far-end signal to lock the bridge. That is, a car must obtain two signals to enter the bridge. When the car has entered the bridge, it releases the near-end signal so that the latter car can obtain it. When the car leaves the bridge, it releases the far-end signal. UFCFYN-15-M-Analysis and Verification of Concurrent Systems 5 You need to redesign the processes for the cars and the bridge to allow the signal events, and use the refinement to prove the safety property. The new system with the signals should be given in FDR with the related safety property refinement. Task 1.4: (15%) Verify the system with the signals from Task 3 is deadlocked free. If you can find the deadlock in the system from the model checking, you can redesign the behaviour of a car or introduce another controller or mechanism to avoid the deadlock. Model your modification in FDR with the refinement. Note that the modified system must hold all the properties from the previous task. Three jobs should be done: The refinement of deadlock freedom for the system The modification of related processes to avoid deadlock The new refinement of the modified system to prove its deadlock free Task 1.5: (10%) We extend the system by adding more cars here, and we assume there are SIX red cars and SIX blue cars. One potential problem for the design in Task 4 is that a certain group of cars may get an advantage than another group to obtain the signals. Therefore, you need to design a fairer controller which allows three cars with the same colour maximally to go through the bridge, and then pass the signals to the cars with another colour. Model such a controller in FDR, and verify it by showing the traces with more than three cars in the same direction is not allowed. Task 1.6: (5%) Produce a mini report to explain and discuss your design or any issue from Task 1.1 to Task 1.5. For example, you may explain some tricky parts of the CSP scripts to enable the reader to understand why this design satisfies the requirements of the tasks. This report should be 800 words maximum