Parking system

This example is studied here. It describes the management of a car park. We adopt a bottom-up approach to design the components of the system. The components and their parallel compositions are successively checked against consistency and compatibility. Additionally we check by refinement a correctness property and a timing liveness property.

The system is composed by four components: an EntryGate, an ExitGate, a gate Controller and a Payment machine. Each is described by a set of requirements given in natural language. The system is parameterized by the capacity N of the parking. However we adopt an abstract view in which cars are not individualized. The structure of the system with the communication channels between the components is described in the figure below:

Parking components and communications channels

The initial requirements for each component are listed below. For each gate:

• A vehicle shall not pass when the gate is closed.
• Once a vehicle has passed the gate, another vehicle cannot pass before the gate closes.
• After the gate has opened, it does not open before it closes. After the gate has closed, it does not close before it opens.
• The gate must close within 5 seconds after a vehicle passes, and only then.

Specific to EntryGate:

• An entry ticket is issued only when the entry gate is closed.
• The gate must open within 5 seconds after an entry ticket has been issued, and only then.

Specific to ExitGate:

• An exit ticket is inserted only when the entry gate is closed.
• The gate must open within 5 seconds after an exit ticket has been inserted, and only then.

For Controller:

• A vehicle does not exit when the parking is empty.
• A vehicle does not enter before receiving an entry ticket.
• If the parking is not full, an entry ticket is issued within 10 seconds after being requested.

For Payment:

• A user inserts a coin every time an entry ticket is inserted and only then.
• A user may insert an entry ticket only initially or after an exit ticket has been issued.
• The payment machine issues an exit ticket within 40 seconds once the entry ticket and the coin have been inserted.

Each requirement yield a timed automata specification. This specifications are compose with conjunction operator in order to build the model of each components. Then the system is build using the parallel composition between each components. Additional requirements are added during the analysis to specify the behaviour of the environment. We can analyse the consistency of each components and the compatibility between them.

Finally we check the correctness, express by the property that no vehicle can exit the parking without paying. This property is described by the specification SpecExp shown below, and we check that:

We also check a timing property SpecTime that specifies that there is a maximal time bound between a car entering the parking and a car exiting.

SpecExp	SpecTime