Description:
The Direction Of Movement property specifies that the controller orders the car to move in the correct direction. This means that it is never the case that the controller records the correct direction of movement as being down and then orders the car to move up or conversely that it is never that case that the controller records the correct direction of movement as being up and then orders the car to move down. We chose the first option.
This property should be valid when analyzed by any of the finite state verification tools.
Specification:
Back to Concurrent Elevator
Back to main