CA648 Formal Programming

Practical 8: Traffic Lights

Aim

The aim of this practical is to gain further experience in producing refinements of Event-B specifications, and in proving that these refinements are correct with respect to the original specifications.

Traffic Lights

This practical is concerned with specifying and refining a model of traffic lights.

Initial Model:  A Simple Four Way Intersection

Consider a four-way intersection with traffic light control in the two directions EastWest and NorthSouth. The lights in the East and West directions are identical; similarly with North and South.

Specify a model of these traffic lights consisting of the following:

Two enumerated sets:

DIRECTION = {NorthSouth, EastWest};

LIGHT = {Red, Green, Amber}

A variable lights, which will model the relation between directions and the lights showing in those directions.

An invariant:

lights : DIRECTION --> LIGHT

and an expression of the safety condition that when a Green or Amber light is showing in

            any direction then Red must be showing in the other direction.

            The light sequencing is: Red, Green, Amber, Red, . . .

An appropriate initialisation.

The following events should be handled:

ToRed(dir): an event that sets the light to Red in direction dir

ToGreen(dir): an event that sets the light to Green in direction dir

ToAmber(dir): an event that sets the light to Amber in direction dir

            Each event must have appropriate preconditions that ensure that the safety conditions will be

            met. The proof obligations will contain checks of the consistency of the machine invariant

            and the operations.

First Refinement: An Intersection With Right-Turn Lights

Suppose that we now wish to add right-turn lights in the North and South directions.

Change DIRECTION to contain {North, NorthRight, South, SouthRight, EastWest},

recognizing that we now need to split the NorthSouth direction into four directions.

Change the rest of the model.

Second Refinment:  A Generic Intersection With Multiple Undetermined Directions

Change DIRECTION to a carrier set, i.e. no identified specific directions.

Add a constant conflicts: DIRECTION <-> DIRECTION

conflicts relates a direction to all other directions that conflict with that direction. .

Add more predicates that identify properties of conflicts.