Concurrent Elevator Problem

DESCRIPTION

The Concurrent Elevator problem models the behavior of an elevator system installed within a building. There is a controller task that is responsible for a single car task. The controller task accepts requests from the passengers and dispatches the car appropriately. The car task accepts requests from its passengers and forwards them on to the controller task. A car task acknowledges the following commands from the controller: open/close doors, move up/down, continue in the current direction, and stop. This means that ultimately the controller task is responsible for the correct and safe functioning of the elevator system.

Our implementation of this problem uses two tasks: one for the controller and one for the car. This problem is not scalable.

ADA SOURCE

The size indicates the number of cars. There is a single size for this problem. This means that there are two tasks the controller and the car.

size : 1

PROPERTIES

Some specific properties are provided below:

• Direction Of Movement
• Not Move With Doors Open
• Opens Doors When Ordered To Stop

The property specifications by formalism are:

• Computation Tree Logic ( CTL )
• INCA Query
• Never Claims
• Quantified Regular Expression ( QRE )

Back to main