![]() |
![]() |
Frédéric Mallet > M1 IFI - M7 - Mobile & Embedded Systems > Traffic light with NuSMV
Traffic light with NuSMVDe $1Table des matièresSimple traffic lightNote : NuSMV accepts only Mealy Machines ! The system has three actors:
The traffic light controller is in charge of computing the behavior of the car and pedestrian lights:
Initially the car light is red. 5 ticks after turning red, the car light turns green. It remains green during ten ticks before going to yellow. It remains yellow during 2 ticks before turning red again.
The control of the pedestrian light does not directly depend on the time (tick). It must be done in a way that is safe for the pedestrians to cross the street. P1 [Safety]: The pedestrians must not be able to cross when the car light is either green or yellow. P2 [Liveness]: The pedestrians must be able to cross the street at some point: the pedestrian light turns green infinitely often assuming that ticks occur infinitely often. A - Functional verification
Traffic Light extensionInstead of having the car light turning back to yellow and red automatically after some ticks, we would like to build a smart light controller that goes back to red only when a pedestrian has pushed a button. To avoid having the cars being interrupted too frequently, the car light must remain green at least 10 successive ticks, whether there is a pedestrian or not.
Mots clés:
|
Powered by MindTouch Deki Open Source Edition v.8.08 |