Question

In finite state model, of a traffic-light controller and verify its properties using a symbolic model-checker; we need to:

•Assume that the controller manages traffic and pedestrian lights at the intersection of two roads, both with two-way traffic.

•Pedestrians can request access to cross the road by pressing a “walk button”.

•Assume that the system has traffic sensors for each direction to detect if vehicles are present and waiting to pass through, which allows the system to manage traffic flow efficiently by varying the amount of time the lights are green for each road/direction based on demand. Your model should capture and represent this notion of varying time in some manner (i.e., do not abstract away time).

•There are emergency vehicle sensors for each direction which lets the system provide priority access for emergency vehicles by switching lights appropriately.

How would you begin to Define the scope and the requirements for the system that you intend to model? Assumptions? Key Requirements?