18649 - High Level Requirements Verification

18649 Fall 2015
Group 12 - Tom Eliot (tke), Shepard Emerson (semerson), Daniel Gorziglia (dgorzigl), Daniel Haddox (dhaddox)

Verification Framework Description

The high level requirements are checked constantly as the elevator runs. This is achieved through a runtime monitor. The runtime monitor consists of multiple event-based statecharts that transition to error states when requirements are violated. The statecharts contain only two states, one for nominal operation and one for violated requirement.

R-T6: The Car shall only stop at Floors for which there are pending calls.

The statechart transistions to the error state when the elevator stops and there is no hall call or call call for that floor. The statechart returns to the nominal operation state when the elevator begins moving (but not leveling) again.

R-T7: The Car shall only open Doors at Hallways for which there are pending calls.

This statechart is duplicated for each hallway. The sta.echart transitions to the error state when either door opens and there is no hall call or car call for that hallway. The statechart returns to the nominal operation state when all of the doors closed.

R-T8.1: If any door is open at a hallway and there are any pending calls at any other floor(s), a Car Lantern shall turn on.

This statechart normally tracks the state of the doors, with states for door closed and door fully open. It will transition to the error state from the door open state if there are any calls in the system and the lantern is off, and report a violation.

R-T8.2: If one of the car lanterns is lit, the direction indicated shall not change while the doors are open.

This statechart has three states: doors closed, up lantern on, and down lantern on. It transitions to the up/down lantern on states when the lanterns light and the doors are open. If a transition occurrs between the up/down lantern states, a violation will be reported.

R-T8.3: If one of the car lanterns is lit, the car shall service any calls in that direction first.

This statechart starts in the lantern off state. If either the up or down lanterns light, it transitions to those respective states. Once the lantern turns off, the statechart wil transition to the latch state, where it then waits for the drive to be commanded. If, before the drive is commanded, the car lantern turns back on, the statechart will reset to the lantern off state then go back to the proper lantern on state. From the latch state, if the drive is commanded to the same direction as the lantern, the statechart will transition to the going up/down state then immediately transition back to the lantern off state. If the drive is commanded to the opposite direction as the lantern, the monitor checks if there were calls in the same direction as the lantern, and reports a violation if there were. Then, the statechart transitions to the going up/down states then immediately back to the lantern off state.

R-T9: The Drive shall be commanded to fast speed to the maximum degree practicable..

This statechart initializes into the stopped state. When the elevator starts moving, it will transition in to the Slow state. If the drive is not commanded to Fast for more than MAX_SLOW_DUR seconds (representative of the worst-case time in the slow state), the requirement will have been considered violated. Normal operation from this state would be to either go back to stopped or go to fast speed. If the elevator transitions to Fast speed, the only thing that can happen next is for it to slow again, sending the statechart into the slowing state. Again, if the elevator remains in this state for more than MAX_SLOW_DUR seconds, the violation will have been considered violated. It will also have been considered violated if the elevator goes back into the fast state from the slowing state. Under normal operation, the elevator will then transition back to the stopped state when it has stopped.

R-T10: For each stop at a floor, at least one door reversal shall have occured before the doors are commanded to nudge.

The statechart keeps track of four conditions: doors closed, doors opening, doors closing, and doors nudging, and is replicated for each hallway. The statechart initializes into the closed state, and openings, the total number of openings per cycle, is set to zero. When the doors start opening, the statechart transitions to the opening state, incrementing the openings count. Then, when the doors start closing, the statechart will transition to the closing state. If a reversal occurs, the statechart will transition back to the opening state and increment the openings count again. If this happens, the doors will begin to nudge, and the statechart transitions to the nudging state. In this case, openings was greater than one (2), so no violation was reported. However, if the doors had transitioned to the nudge state without a reversal having happened before, the openings count would only be one, and a violation would be reported.

Verification Instructions

To use the runtime monitor, run the elevator simulator with the command "-monitor RuntimeRequirementsMonitor". This will check all of the requirements as the elevator runs. Running the simulator with a variety of acceptance tests and seeds will give better test coverage.

Verification Results

Acceptance Test Name	Verification Status	Link to Verification Results	Notes
proj7acceptance1.pass	pass	proj7acceptance1.stats	No high-level requirement violations past startup transients.
proj7acceptance2.pass	pass	proj7acceptance2.stats	No high-level requirement violations past startup transients.
proj7acceptance3.pass	pass	proj7acceptance3.stats	No high-level requirement violations past startup transients.
proj8group12acceptance1.pass	pass	proj8group12acceptance1.stats	No high-level requirement violations past startup transients.