17-07-2012, 04:56 PM
Traffic Light Controller Examples in SMV
traffic.ppt (Size: 2.78 MB / Downloads: 223)
Plan for today
Modeling Traffic Light Controller in SMV
Properties to Check
Four different SMV models for traffic light controller
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
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
Some more variables
To ensure mutual exclusion
We will have two Boolean variables
NS-Lock: denotes locking of north/south lane
EW-Lock: denotes locking of west lane
To remember that there is traffic on a lane
Boolean variables: N-Req, S-Req, W-Req
If N-sense becomes 1, then N-Req is set to true
Similarly, for others….