Mode logic - lgwagner/SpeAR GitHub Wiki

Table of Contents Introduction Imports Inputs Outputs State Macros Assumptions Requirements Properties

This specification file in the microwave oven example defines how the mode logic state machine will behave, a critical piece to ensure that safety is maintained.

Here only the single import is necessary to have access to the global data types.

The inputs to this component provide the current information from the user and the current internal information. Remember that this analysis technique looks at the current moment in time (the current time step). Therefore at every time step this component requires the state of four different inputs to properly determine the current mode. One can ask themselves four separate questions to determine the input values: (1) was the clear button pressed (2) was the start button pressed, (3) is the door closed, and (4) how many second remain to cook?

The two outputs provide the mode state of the system as well as the value of the component's calculation of seconds_remaining.

None necessary for this component.

The macros listed here make the definitions of the requirements more natural for the user. In order to determine changes in mode or time the value of the previous time step is compared with that of the current time step.

The assumption that this component will only be called when the seconds left to cook is greater than or equal to 1 is enforced here.

Again the requirements here define the behavior of the component. Requirement r1 defines how the microwave time is affected by the mode that it is in. The other requirements establish specific modes of the appliance dependent on keyboard inputs, door state, and previous mode states.

Property p1 is the safety property at this component level; it ensures that that door cannot be open and the device in a COOKING mode. The other properties maintain definition based qualities and also initial state of the system.