Microwave - lgwagner/SpeAR GitHub Wiki

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

This is the main specification file for the microwave oven system. It is designed to utilize sub-components to capture specific behavioral aspects while this file establishes the interaction of the of those components in the system.

NOTE: Description of this file will progress through the sections from the top of the file to bottom. This is not necessarily how the file was constructed but rather how it is organized.

There are five imports into this file, each defining either a component defined in another specification file or a definitions file that makes common data types available to this file.

Viewing the microwave oven as a system, the user has two ways to directly influence the system state: (1) through opening and closing the door or (2) by pressing the keys of the keypad. For simplicity the option to unplug the system is not a viable user input. It is assumed that the system has sufficient power throughout this exercise (the microwave is plugged in).

The system outputs to the user comprise the displayed countdown time left in the COOKING mode. To define this display there are three different single digit display numerals: left_digit, middle_digit, and right_digit.

These are the local state variables of the specification. This section is ideal for any state information that must be maintained internal to the specification but is not necessary outside the component.

Often the best time to use macros is to simplify a call to a complex state. For example, to be able to determine if the microwave should be cooking, the amount of time remaining to cook is something that must be questioned. As it was previously mentioned, the displayed time is not presented to the user most of the time in seconds but in M:SS format. In order to determine the total seconds remaining, the calculation of (left_digit*60 + middle_digit*10 + right_digit) would need to be used every time. With a macro, seconds_to_cook abstracts that calculation for the user. This often improves the readability of the formalisms for which a macro is used.

No assumptions are defined in this file but if there was a desire to capture an assumption this is where it would be. Remember, assumptions are a way to provide information to the specification ways in which the inputs are valid. For example, providing a negative time to timer does not make sense in this system but the model checker conducting the analysis does not have that understanding; it must be provided.

The requirements section can often be thought of as where the behavior of the component is defined. In a specification file, the sub-components of a system can be hoisted by inclusion into an equivalency check. For example, in the microwave.spear file, look at r1. The mode logic component, when provided inputs of two boolean macros (clear, start), one input (door_closed), and an integer macro (seconds_to_cook) will provide two outputs (microwave_mode, seconds_remaining) to this specification. Requirements rl to r5 represent all the sub-components being used to by this specification to handle behaviors in a compositional fashion.

Note - In order to assign a hoisted spec call that has a single output the vertical pipes (|) are not needed about the single value. Only when a spec returns multiple outputs are the pipes necessary (as shown in this example).

The properties section establishes what should be held throughout the execution of the specification. All the requirements define what the properties will test (using model checking) to determine if a violation can occur. The most straight-forward types of properties are those that define the safety of the system (known as a safety property). Other types, are definitional in that they ensure that behavioral requirements are properly defined and bounded. In the microwave example, p0 is the most critical safety property; if the microwave is cooking the door must be closed. Any violations of this property would introduce an unsafe situation upon the user. Properties p2 to p4 ensure that the the outputs to the user cannot violate the numeral range requirements and are a definitional protection on the system. The final properties, p_init and p1, establishes the initial state of the microwave, thus ensuring that at power-up (plugging in) the device does not have any capability to be in a dangerous mode.