Traffic Light Controller Examples in SMVPlan for todaySlide 2Slide 3Slide 4Slide 5Slide 6Slide 7Slide 8Let’s see how to model all this in SMVSlide 10Slide 11Properties we would like to checkSlide 14Slide 14Slide 15Fairness ConstraintsNow we look at some concrete implementationsSome more variablesTraffic1.smvSlide 20Module south is similar Module west1 is a little different Everything seems ok!Mutual exclusion fails (Counterexample)Slide 24Slide 25Slide 25This problem is fixed in traffic2.smvModel checking traffic2.smvCounterexample for liveness property contains a loopSlide 30Ensuring liveness requires more workSlide 31Model check againSlide 34Traffic4.smv Slide 35Hurray!Think aboutQUESTIONSTraffic Light Controller Examples in SMVHimanshu JainBug catching (Fall 2007)2Plan for todayModeling Traffic Light Controller in SMVProperties to CheckFour different SMV models for traffic light controller3NSWScenario4NSWNo turning5NSWBinary traffic lights6NSWSafetyPropertyThis should nothappen7NSWSafetyPropertyThis should nothappen8NSWLivenessPropertyWhen will the stupid light become green again9NSWLivenessPropertyThank God!Traffic in each direction must be served10Let’s see how to model all this in SMV11NSWSMV variablesN-go=0S-go=0W-go=1Three Boolean variables track the status of lights12NSWSMV variables Three Boolean variables sensethe traffic in each directionN-sense =1S-sense =1W-sense =0These variables are called N, Sy, W in thecode I will show you13Properties we would like to checkMutual exclusion SPEC AG !(W-Go & (N-Go | S-Go))Liveness in North directionSPEC AG(N-sense & !N-Go -> AF N-Go)Similar liveness properties for south and west14Properties we would like to checkNo strict sequencingWe don’t want the traffic lights to give turns to each other (if there is no need for it)For example, if there is no traffic on west lane, we do not want W-go becoming 1 periodicallyWe can specify such properties atleast partiallyAG(W-Go -> A[W-Go U (!W-Go & A[!W-Go U (N-Go | S-Go)])])See code other such propertiesWe want these properties to FAIL15NSWSMV modulesNorth modulewill control South modulewill control West modulewill control Main module will-Initialize variables-Start north, south, west modules16NSWWhat if north light is always green and there is always traffic in north direction17Fairness ConstraintsWhat if north light is always green and there is always traffic in north directionWe will avoid such scenarios by means of fairness constraintsFAIRNESS running & !(N-Go & N-sense)On an infinite execution, there are infinite number of states where either north light is not green or there is no traffic in north directionSimilar, fairness constraints for south and west directions18Now we look at some concrete implementations19Some more variablesTo ensure mutual exclusion We will have two Boolean variablesNS-Lock: denotes locking of north/south laneEW-Lock: denotes locking of west laneTo remember that there is traffic on a laneBoolean variables: N-Req, S-Req, W-ReqIf N-sense becomes 1, then N-Req is set to trueSimilarly, for others….20Traffic1.smvMODULE mainVAR N : boolean; --senses traffic going along north Sy : boolean; --senses traffic going along south W : boolean; --senses traffic going westward N-Req : boolean; --rememebers that there is traffic along north that needs to go S-Req : boolean; --rememebers that there is traffic along south that needs to go W-Req : boolean; --rememebers that there is traffic along west that needs to go N-Go : boolean; --north direction green light on S-Go : boolean; --south direction green light on W-Go : boolean; --west direction green light on NS-Lock : boolean; --north/south lane locked EW-Lock : boolean; --east/west lane locked north : process north1(NS-Lock, EW-Lock, N-Req, N-Go,N,S-Go); south : process south1(NS-Lock,EW-Lock,S-Req,S-Go,Sy,N-Go); west : process west1(NS-Lock,EW-Lock,W-Req,W-Go,W);ASSIGN init(NS-Lock) := 0; init(Sy) := 0; init(W) := 0; init(W-Req) := 0; …………………..OTHER INITIALIZATIONS21MODULE north(NS-Lock, EW-Lock, N-Req, N-Go,N,S-Go)VAR state : {idle, entering , critical , exiting};ASSIGN init(state) := idle; next(state) := case state = idle : case N-Req = 1 : entering; 1 : state; esac; state = entering & !EW-Lock : critical; state = critical & !N : exiting; state = exiting : idle; 1 : state; esac; next(NS-Lock) := case state = entering & !EW-Lock : 1 ; state = exiting & !S-Go : 0; 1 : NS-Lock; esac; next(N-Req) := case !N-Req & N : 1; state = exiting : 0; 1 : N-Req; esac; next(N-Go) := case state = critical : 1; state = exiting : 0; 1 : N-Go; esac;-- non-deterministically chose N next(N) := {0,1};FAIRNESS running & !(N-Go & N)22Module south is similarModule west1 is a little differentEverything seems ok!Let us run a model checker23Mutual exclusion fails (Counterexample)1. All variables zero2. N-sense=1 (North module executed)3. S-sense=1 (South module executed)4. S-Req=15. south.state=entering6. S-sense=0, NS-Lock=1, south.state=critical7. S-sense=1,S-go=1,south.state=exiting8. N-Req=19. north.state=entering10. north.state=critical11. S-Req=0, S-Go=0, NS-Lock=0, south.state=idle12. W=113. W-Req=114. west.state=entering15. EW-lock=1, west.state=critical16. W-Go=117. N-Go=1One module is executing at each step24Mutual exclusion fails (Counterexample)1. All variables zero2. N-sense=1 (North module executed)3. S-sense=1 (South module executed)4. S-Req=15. south.state=entering6. S-sense=0, NS-Lock=1, south.state=critical7. S-sense=1,S-go=1,south.state=exiting8. N-Req=19. north.state=entering10. north.state=critical11. S-Req=0, S-Go=0, NS-Lock=0, south.state=idle12. W=113. W-Req=114. west.state=entering15. EW-lock=1, west.state=critical16. W-Go=117. N-Go=1One module is executing at each stepEven though north.state is critical the NS-lock is released25Mutual exclusion fails (Counterexample)1. All variables zero2. N-sense=1 (North module executed)3. S-sense=1 (South module executed)4. S-Req=15. south.state=entering6. S-sense=0, NS-Lock=1, south.state=critical7. S-sense=1,S-go=1,south.state=exiting8. N-Req=19. north.state=entering10. north.state=critical11. S-Req=0, S-Go=0, NS-Lock=0, south.state=idle12. W=113. W-Req=114. west.state=entering15. EW-lock=1, west.state=critical16. W-Go=117. N-Go=1One module is executing at each stepOne problem is the
View Full Document