Concurrent Elevator Problem


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.


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


Some specific properties are provided below:


The property specifications by formalism are:


Back to main