Lecture (39 pages)

Previewing pages 1, 2, 3, 18, 19, 37, 38, 39 of actual document. View the full content.
View Full Document

Lecture



Previewing pages 1, 2, 3, 18, 19, 37, 38, 39 of actual document.

View the full content.
View Full Document
View Full Document

Lecture

63 views


Pages:
39
School:
Carnegie Mellon University
Course:
Cs 15414 - Bug Catching: Automated Program Verification and Testing

Unformatted text preview:

Traffic Light Controller Examples in SMV Himanshu Jain Bug catching Fall 2007 2 Plan for today Modeling Traffic Light Controller in SMV Properties to Check Four different SMV models for traffic light controller Scenario 3 N W S 4 No turning N S W Binary traffic lights 5 N W S Safety Property 6 N W This should not happen S Safety Property 7 N W This should not happen S Liveness Property 8 N W When will the stupid light become green again S Liveness Property 9 N W Thank God S Traffic in each direction must be served 10 Let s see how to model all this in SMV SMV variables 11 N N go 0 Three Boolean variables track the status of lights W W go 1 S go 0 S 12 SMV variables N Three Boolean variables sense the traffic in each direction S sense 1 W sense 0 W N sense 1 These variables are called N Sy W in the code I will show you S 13 Properties we would like to check Mutual exclusion SPEC AG W Go N Go S Go Liveness in North direction SPEC AG N sense N Go AF N Go Similar liveness properties for south and west 14 Properties we would like to check No strict sequencing We 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 periodically We can specify such properties atleast partially AG W Go A W Go U W Go A W Go U N Go S Go See code other such properties We want these properties to FAIL SMV modules 15 N West module will control North module will control W South module will control S Main module will Initialize variables Start north south west modules What if north light is always green and there is always traffic in north direction 16 N W S 17 Fairness Constraints What if north light is always green and there is always traffic in north direction We will avoid such scenarios by means of fairness constraints FAIRNESS 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



View Full Document

Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view Lecture and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Lecture and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?