CSCI P415/P515 HW/ITC

CSCI P545

Mon Mar 28 16:04:05 EDT 2011 © [SDJ]

Homework Assignment

This assignment requires a team of two or more people. It has two parts:

Independently design and model in SMV a solution to the Island Traffic Controller problem (below).
Verify each team member's model.

In order to do the second part, everyone must encapsulate both a controller model and its "environmental" constraints in a uniform way. Both are to be encapsulated as SMV MODULEs interacting through a common parameter list, as discussed in greater detail after the problem description.

Island Traffic Controller

This problem is a refinement of the standard Traffic Light Control problem and has also been compared to the Clayton Tunnel Disaster. It is a metaphor for coordinating access to a restricted resource. Concurrent entry/exit is allowed under certain conditions, represented by a one-lane tunnel between the Mainland and an Island that may at any time contain several vehicles. There is a bound on the number of vehicles that may be on the island.

We want to design a controller for the red (MR and IR) and green (MG and IG) traffic lights at the each end of this tunnel. There are four sensors for detecting the presence of vehicles: one at tunnel entrance on the island side (IE), one at tunnel exit on the island side (IX), one at tunnel entrance on the mainland side (ME), and one at tunnel exit on the mainland side (MX).

Environmental Properties

The controller design may assume the following constraints on its environment, described in terms of the behavior of vehicles entering the system.

E1	The vehicle sensors are conditioned signals, that is, clean pulses of significant duration.
E2	Every vehicle that crosses a sensor is detected and every gap between vehicles that cross a sensor is detected.
E3	Vehicles going into the tunnel are detected before they reach the traffic light; vehicles leaving the tunnel are detected after they leave the single-lane portion of the roadway.
E4	Vehicles don't break down. They obey the traffic signals in finite time, and, if necessary, a bound may be placed on this time. Every vehicle that approaches the tunnel is committed to entering it.
E5	Having arrived on The Island every vehicle eventually tries to leave.

Design Properties

D1	Light Behavior. The traffic lights each follow a red, green, red, green, . . . sequence. Since we have not included a ``caution'' light in this model, this property is satisfied trivially. It may also be assumed, for simplicity, that all vehicles can react instananeously to a change in the traffic light, so that explicit duration timers are not needed in this model.
D2	Safety. At no time are there two vehicles in the tunnel that are traveling in opposite directions.
D3	Liveness. Any vehicle attempting to reach or leave the island eventually succeeds.
D4	Access. Traffic on the island is limited. At no time are there more than 16 vehicles on the island.
D4	Single Controller. One may design a single controller for both the mainland and island entries. As a variation, one may optionally require seperate, asynchronous controllers at both ends of the tunnel, and impose constraints on communication bandwidth between them. However, under any such variation, the external signature (IE, IX, IR, IG, ME, MX, MR, MG) of their composition must be preserved.

Modelling Requirements

In addition to verifying your own design, you will be verifying others', under the conditions you have used. Thus, it is essential that everyone have a uniform interface to their designs. Follow these constraints carefully.

Design Model. Code your design model in the form of a SMV module:

      MODULE itc_control(IE, IX, IR, IG, ME, MX, MR, MG) ...

The module name must be itc_control
Boolean parameters must be in exactly the given order.
The module must be self-contained. There may no external variable references within the module.
IE, IX, ME, and MX are input signals; hence there must be no ASSIGN statements affecting them within the control module. They are assigned either at the top level or by other modules in the system.
IR, IG, MR, and MG are output signals. All ASSIGN expressions for these come from within the control instance.
The itc_control module definition must contain no SPEC statements.
There may be no FAIRNESS statements other than FAIRNESS running.

Thus, all restrictions and assumptions about the behavior of the input signals should be external to itc_control module.

It is recommended that you encapsulate these constraints in another module describing the operating environment of the design being verified. You may wish to define a module called environment for this purpose:

      MODULE itc_environment(IE, IX, IR, IG, ME, MX, MR, MG) ...

For itc_environment modules,

IE, IX, ME, and MX are output signals. All ASSIGN expressions for these come from within the itc_environment instance.
IR, IG, MR, and MG are input signals. There must be no ASSIGN statements affecting them within the itc_environment module. They are controlled either at the top level of SMV or by other modules defined in the system.
In addition to FAIRNESS running other FAIRNESS conditions may be used.

In summary, your .smv files should have the following general form

MODULE main

 VAR
 IX : boolean; -- Island   EXIT sensor
 IE : boolean; -- Island   ENTRY sensor
 IR : boolean; -- Island   RED light
 IG : boolean; -- Island   GREEN light
 MX : boolean; -- Mainland EXIT sensor
 ME : boolean; -- Mainland ENTRY sensor
 MR : boolean; -- Mainland RED light
 MG : boolean; -- Mainland GREEN light
 
   
   You will likely need additional variables, for example, to count cars.
  
 -- SYNCHRONOUS interleaving (no "process" keyword) is assumed,
 -- to assure, for example, that the controller detects all sensor readings.
 -- You may have other modules to structure your environment.

 itc : itc_control (ie, ix, ir, ig, me, mx, mr, mg);
 env : itc_environment(ie, ix, ir, ig, me, mx, mr, mg);

 -- Specification statements.  These, too, could be encapsulated
 -- in a module.  It's up to you.

 SPEC -- safety
 SPEC -- liveness
 SPEC -- etc.

 MODULE itc_environment(IE, IX, IR, IG, ME, MX, MR, MG)
 
   Your code here

 MODULE itc_control(IE, IX, IR, IG, ME, MX, MR, MG)
 
   Your code here

The Assignment

Part A Write your controller and environment modules and your correctness specifications.

Part B Once you are satisfied that everything is right, send the source of your itc_control only to the instructor. All control modules will be posted. Verify each module in composition with your itc_environment module. Summarize the results in a report.

You may but are not required to describe any failures in terms of observable signals IX, IW, IR, IG, MX, ME, MG and MR only In other words, do not "debug" others' modules. IX, but do not

Discussion points

To reduce the model checking times, set the limit on the number of cars on the island to 3. However, your controller should be able to handle limits up to 15 cars.
Synchronous semantics should be used in order to guarantee that the controller sees all the changes on the sensor signals.