Formal methods 2014/2015. Homework «Development and verification of light traffic controller». Section 1. Introduction. In this homework, you need to develop a traffic light controller for crossroad management. Each road lane is controlled by its own small controller. Sensors on the road lanes detect presence of cars. When there are no cars on a lane, the traffic light is red. Similar sensor controls pedestrian lane. When cars or pedestrians appear on a lane, the process of the lane traffic light starts to compete for the resources. The resources are parts of the crossroad where lanes cross. If process received needed resources, it switches its traffic light to green allowing movement along its lane. The core of the work is to develop correct algorithms for capturing and releasing resources in traffic light processes. The homework consists of development of traffic light controllers that solve the described problem of traffic controlling with several crossing lanes and pedestrian crossing. Each controller consists of several parallel processes-controllers (for each direction) and global sharing variables, which can be modified and read by these processes. Each traffic light is controlled by its own process. A traffic light process allows or restricts movement along the direction. One of the local variables holds value that is permissive (green) or prohibitive (red) color linked with traffic light process. Global variables are utilized to implement the processes synchronization algorithm. Such algorithm must guarantee the correct usage of shared resources among processes. You can use the implementation for the trivial crossroad in the Section 2 as the starting point for your solution. In the Section 3, you can find the scheme of the more complex crossroad with the several crossing directions. Each student receives his/her own configuration with several crossing lanes defined by capital letters of the from/to directions (NW – from North to West). Other lanes of the crossroad on the scheme can be ignored. A sensor detects cars presence on its direction. If there are no cars, all traffic lights are red. Similar sensor detects presence of pedestrians. If there are no pedestrians, the pedestrian traffic light is red. When a car or a pedestrian appear, the traffic light processes start to compete for the resource "crossroad". The processes that captured the resource turns on green light and the cars (or pedestrians) start movement. The assignment is to develop an algorithm for the controller (which consists of smaller controllersprocesses for each traffic light) that controls the whole crossroad and check its correctness against given live and safety properties. To complete the homework, you need to: 1. construct the model of the crossroad controller with the PROMELA language for your lanes configuration; 2. verify the result model via SPIN; 3. in case of found defects, fix the controller algorithm to obtain the correct algorithm. Section 2. Algorithms for controlling light traffics of the trivial crossroad. You may use the algorithms of this section as the starting point for your solution.2 FIGURE 1. THE TRIVIAL CROSSROAD SCHEME. Let us construct a controller for the traffic lights of the crossroad in Fig.1. The controlled traffic lights are N (to North), S (to South), E (to East), and P (pedestrian crossing). The external events N_SENSE, S_SENSE and E_SENSE, P_SENSE displays that the corresponding sensor found queue. Movement on the given direction is allowed when the corresponding traffic light is green. In this case: a) cars don't turn on the crossroad, but only cross it directly; b) traffic lights have two colours: red-green-red-green… c) pedestrians cross the road only in one place. Controller will consist of four parallel processes: N, S, E, and P. Each process controls its own traffic light, which allows the movement along its direction. Controller's output is the assignment of the light traffic variables – the local variables of the N_LIGHT, S_LIGHT, E_LIGHT, and P_LIGHT processes are assigned to RED or GREEN. Process N reads and can reset its own local boolean variable N_REQ, which shows that north direction is requested. This variable is set by the event N_SENSE: while true do if (!N_REQ && N_SENSE) then N_REQ := true fi od This loop is executed in the process that models external environment. Such process is executed in parallel with N. The same for other processes S, E, and P. To synchronize processes, we need variables shared among all processes. Let us introduce global boolean variables (directions' flags) – NS_LOCK and WE_LOCK. Processes N, S, and E will communicate through these shared boolean variables. All processes below are written in the Pascal-like language. Algorithm of the process N for the north direction can be represented as: process N (){ while true do /* endless loop */ if ( N_REQ ) /* if the north direction is requested */ wait ( !WE_LOCK ); /* wait until crossing direction is free, */ NS_LOCK := true; /* set up the lock for the NS direction */ N_LIGHT := GREEN; /* allows movement on north direction; */3 wait ( !N_SENSE ); /* wait until all cars are passed to the north */ if (S_LIGHT=RED) NS_LOCK := false fi; /* if traffic light on the opposite direction is red, clear the lock */ N_LIGHT := RED; /* set the color of own light traffic to red */ N_REQ := false; /* reset the request for the north direction */ fi od } S can be constructed in much the same way. Algorithm of the process E for the east direction: process Е (){ while true do /* endless loop */ if ( E_REQ ) /* if there is a request for the east direction */ WЕ_LOCK := true; /* then set up the lock */ E_LIGHT := GREEN; /* and allow the movement to the east */ wait( !NS_LOCK ); /*wait until N and S processes reset their lock*/ wait( !Е_SENSE ); /* wait until all cars are passed to the east */ WЕ_LOCK := false; /* reset own lock */ E_LIGHT := RED; /* set up the traffic light to red */ E_REQ := false; /* reset the request for the east direction */ Fi od } These algorithms look reasonable, but their correctness has not been proven. As in any parallel system, the probability of intrinsic defects is high. Moreover, it does not take into account the pedestrian crossing. If during verification some defects are found, they shall be fixed. Section 3. The homework assignment. The crossroad scheme. In your homework, you will consider more complex crossroad with four two-way directions. For each direction, there are three lanes for three possible trajectories: to pass the crossroad without turning; turning right; turning left. Each of these three lanes is controlled by its own traffic light – one for moving forward; one for turning left; and one for turning right. And still there is a pedestrian crossing. For NW and WS directions, turning right is always allowed. But the traffic light must be red, if there are no cars on the lane even. The pedestrian crossing on SE and EN directions must be handled more carefully. When cars appear, it switches to green until the car traffic is ended. When the car traffic is ended, the traffic light switches back to red. For each trajectory (ex. SW) a traffic light turns green if the next conditions are valid: 1. there is a request from the cars on the lane; 2. movement is prohibited on all lanes that crosses the trajectory (ex. ES, WN, NS) , i.e. the corresponding traffic lights are red;4 FIGURE 2. CROSSROAD SCHEME. Each student has its own lanes. Such lanes are chosen from the rows of the table below. You will have several numbers and you have to consider the crossroad configuration with the lanes from the corresponding table rows. Pay attention to the lines that cross the pedestrian crossing. 1 WN,NS 9 SN,WE 2 WN,NE 10 SN,EW 3 WN,SW 11 SN,ES 4 WN,EW 12 NE,EW 5 NS,SW 13 NE,ES 6 NS,WE 14 SW,WE 7 NS,EW 15 SW,ES 8 SN,NE 16 WE,ES You have to ask your instructor for your configuration! Suppose that your configuration is 1 + 10. Than your configuration consists of WN, NS, SN, EW lanes. All other lanes can be ignored. You have to submit the picture of you configuration as part of your solution. You have to model/describe your controller's processes in PROMELA language. As the starting point, you can take the example solution for the trivial crossroad from the Section 2. Note that the example crossroad solution is written not in PROMELA language. There are possibly some synchronization bugs in the solution for the trivial crossroad (you have to check it!). You need to find all bugs with SPIN verification system (demonstrate it with screenshots), and use counterexample trails to find the location of the bug (attach such trails to your reports). A counterexample trail shows the scenario of crossroad traffic when traffic lights work incorrectly.5 Additional requirements for controller model: 1) You must use separate "environment" processes (one for each lane) that control cars and pedestrians appearance; and, separate processes for lane controllers (for each lane) that control the crossroad traffic for each lane; 2) You must not use ``atomic''. You can use the atomic construction only for technical debug purposes (output the value of the variable immediately after its change). It is explicitly prohibited to use it for solving synchronization/concurrency problems. In other words you can use it only if you solution works without atomic constructions. Yes, it is possible to do the homework without usage of atomic at all. Section 4. Algorithm verification. Controller properties. You have to check the correctness of your controller against the next properties: Safety: Movement must never be allowed simultaneously on crossing lanes. G !(( N_LIGHT=GREEN || S_LIGHT=GREEN) and (E_LIGHT = GREEN)) – Liveness: When a car or a pedestrian appears on a lane, it will get an opportunity to cross the crossroad after some finite amount of time. G ( N_SENSE and ( N_LIGHT=RED ) ⇒ F ( N_LIGHT=GREEN ) ); G ( S_SENSE and ( S_LIGHT=RED ) ⇒ F ( S_LIGHT=GREEN ) ); G ( E_SENSE and ( E_LIGHT=RED ) ⇒ F ( E_LIGHT=GREEN ) ); G ( P_SENSE and ( P_LIGHT=RED ) ⇒ F ( P_LIGHT=GREEN ) ); These properties have to be satisfied under the next restrictions (conditions): Fairness: On each lane, the car traffic is not continuous, i.e. each sensor is reset to false infinitely often. GF !( (N_LIGHT=GREEN) & N_SENSE ); GF !( (S_LIGHT=GREEN) & S_SENSE ); GF !( (E_LIGHT=GREEN) & E_SENSE ); GF !( (P_LIGHT=GREEN) & P_SENSE ); You must submit your model (.pml) and a report (.docx/.pdf). Report includes: 1. the picture of your configuration; 2. narrative description of how did you model the traffic light system (1-3 paragraphs); 3. narrative description of how did you secure each of the next properties in your system (1-2 paragraph for each property): a. safety; b. liveness; c. fairness; 4. appendix with all verification results for all LTL properties;6 5. conclusion on what was the most complex part of the problem for you to solve.