Problem Frame Transformations: Deriving Specifications from Requirements

The unit has four physical lights: a red and a green in each direction. The control unit sends signal pulses to the light unit to toggle the four lights on and off. The cars mov-ing in each direction observe those traffic signals, and then
decide whether or not to enter the road segment. The end-to-end requirement is that cars do not collide, which we will interpret to mean that no two cars are ever in the intersec-tion at the same time going opposite directions. However,
the control unit has no knowledge of, or control over, the cars; it can only send signal pulses to the light units and ob-serve the history of what signals it previously sent. So what specification should the control unit be expected to uphold? In Figure 6, the Problem Frame description has been formalized; the phenomena have been concretized and the requirement specified in formal language. For example, NRpulse(t) designates that a signal pulse was sent to the
control unit at time t to toggle whether the northward facing red light is lit or not. NRobserve(c, t) designates that a car c observes the northward red light to be lit at time t. CarOnSegment(c, t) designates that a car c is on the road
segment at time t. CarDirection(c, t) designates the di-rection car c is moving, and can evaluate to either north or south.