Figure 11.1 The car parking system
to the devices. The computer executes a control program that coordinates
the physical devices in order to prevent cars entering the parking area
without a ticket.
The physical devices
The semaphore is a standard two-colour traffic light. It behaves as a finite
state machine that has two states, RED and GREEN , and two state transitions
A photocell is a simple device made up of an optical sensor that detects
the light beam of a transmitter. The sensor and the transmitter are po-
sitioned at the opposite sides of the access lane. When a car enters the
sensor zone, it interrupts the light beam. When the car leaves the sensor
zone, the sensor detects the light beam. Thus, a photocell behaves as a finite
state machine that has two states, CLEARED and OCCUPIED , and two state
transitions between them. Whenever a state transition occurs, the device
sends a signal to the computer. We assume that a photocell is a reliable
device that always behaves according to these specifications.
The ticket dispenser is a machine that delivers a ticket when it receives a
command from the controller. The dispenser delivers only one ticket at a
time. When the driver withdraws the ticket, the dispenser is ready to deliver
a new one. It can be modelled as a finite state machine with two states,
DELIVERED and WITHDRAWN , and two transitions between them. When a
state transition occurs, the machine sends a signal to the computer.
The stopping bar receives two commands from the controller, raise and
lower and signals the controller when it reaches the UP and DOWN positions.
We assume that the stopping bar is an unreliable device that might be
unavailable for certain periods of time when the intervention of the operator
The car and the driver
The car represents the external world that sends stimuli to the access
control system and receives feedback from it. The car sends stimuli to the
photocells, when it occupies and clears the sensor zones, and to the ticket