Communicating Sequential Processes assignment (using kiltera)

General Information

The assignment: Process-oriented modelling

The purpose of this assignment is to build a model of a system specified informally.

The formalism to be used for the model is kiltera (a link to kiltera's website is provided below.) The system to be modelled consists of a traffic light, a pedestrian and the police. The system is specified as follows:

A normal traffic light alternates between three basic states: green, yellow and red. The system remains in each state for a specific amount of time (which should be a parameter.) In addition to this basic operation, the traffic light must take into account some extraordinary situations: first, the traffic-light may be on or off and it must have a switch to change between these two states. Second, it has a "crosswalk" button, which is enabled only when the light is green and when pushed will turn to red after a couple of seconds (also a parameter.) This is to enable a pedestrian to cross. Aside from the normal behaviour described above, the traffic-light has an alternative mode of operation which can be activated by police in case of emergencies. In this alternative mode, the traffic-lite flashes its yellow light, i.e. the yellow light turns on and off again and again (with some fixed amount of time.) The traffic light should remain in this flashing mode until signaled by police to return to its normal mode of operation.

Aside from modelling the traffic light itself, we need a model of a pedestrian and police to interact with the traffic-light.

The pedestrian should behave as follows: initially the pedestrian is idle. After a certain given amount of time (a parameter,) it pushes the "crosswalk" button and waits for the light to turn red. When the light is in red for the cars, the pedestrian can cross.

The police will behave as follows: after 20 seconds the police will hit the emergency button. Then after 5 seconds it will hit the button again to return it to its normal mode of operation. Then after another 5 seconds it will turn off the light. Then, after 2 seconds it will turn it on again.

The whole system will have one traffic light, one pedestrian and one police officer.

You can find kiltera's distribution and documentation at: msdl.cs.mcgill.ca/people/eposse/projects/kiltera.

If you have any questions regarding kiltera, contact Ernesto at eposse@cs.mcgill.ca or at McConnell Engineering, room 202.