Table of Contents Example: The Microwave Oven Identification of the Safety Concerns General Layout Suggestions Microwave definitions Microwave Mode logic Keypad processing Reverse time Compute time Component Development Techniques

The majority of people are familiar with the household appliances and their daily use. Even though these appliances are commonplace, the safety of them is taken for granted by most people. One such example is that of the typical microwave oven (typically called a microwave) in which foods are heated through the use of microwave radiation in the electromagnetic spectrum.

There are significant safety concerns should the appliance be activated (or energized) in a state where the shielding is not in place. Should this occur the user would be exposed to radiation that could be harmful.

Here we will demonstrate how to specify the safety properties, behavior, and structure of a basic microwave. By the use of model checking we will demonstrate that the safety properties on the microwave are maintained.

In a microwave the most important safety concerns deal with the use of the electromagnetic radiation. This is mitigated through ensuring the the cooking cavity is enclosed within a wire mesh so as to not allow the radiation to escape. The easiest location of failure of this protection is state of the appliance door. Let's use SpeAR to identify if there is any missing logic that would allow the door to be open while the system is energized.

In model checking, the explosion of states to check is often a limitation on the complexity of systems to be analyzed. Although a significant problem, there are mitigation techniques that will allow for more complexity to be examined. In SpeAR, using compositional verification techniques is highly encouraged.

Compositional verification: The technique to separating a system into logical blocks that can be verified independently (with less complexity than a full system) and then examined as blocks to ensure the entire system functions as expected.

In order to follow this technique the microwave will be represented in SpeAR according to compositional principles. The safety of the overall system is determined if the contractual properties of the sub-components prove safe.

The sub-components of the system will can be seen in the following diagram (generated by the graphviz visualization option). All the components have associated pages so to better describe the roles each fulfills in the appliance.

This is a Definitions file that will define a number of the data types to be used across all the of the component specification files.

This is the overarching Specification file for the complete microwave oven system. The overall safety properties are defined here. The sub-components defining the system are lifted to this file in order for the functionality that each provides to be included in the composed system. How this is accomplished will be discussed in the Microwave.spear file section.

This is the sub-component that governs the current operating mode of the system. Many may find that this component represents a state machine (or automaton) of the control logic of the appliance. For this example there will be three modes of operation; SETUP, COOKING, SUSPENDED. Only one of the modes can be active at any one time.

In the display of simple microwave ovens, the time to cook is represented by a chain of digits that represent the time remaining for the oven to be energized. This component formalizes the behavior of this display with the representation of each digit as composed as part of the remaining time. It also is responsible to ensure that as the time elapses that the digits that are no longer needed is not displayed to the user.

This component translates the internal value of the seconds left in the cooking time to a displayed value for the user in the form of M:SS.

This component provides the system an internal representation of time in seconds. Therefore, any user time input will be captured by the system and converted to seconds.

A common question that is often asked when somebody is first introduced to SpeAR is a concern about how to go about the development of components. Specifically, the concern depends largely on the user's overall view of the system. For instance, when first developing the requirements of a system a SME (subject matter expert) may have no idea at what kind of sub-components are necessary to establish a formal representation of the system. There may only be abstract ideas of the system but there may exist specific safety concerns that must be maintained. Another SME may have a very specific understanding of components but are being challenged at how to assemble these components to produce a more complex system. Both of these development techniques, better known as top-down or bottom-up design, are valid and can prove equally effective. In the microwave example we will attempt to illustrate these techniques.

It is worth noting that in the experience of the authors there are rarely situations where solely a top-down or a bottom-up design is executed completely. What is important is that these techniques refer primarily to the level of fidelity of the user's view. Therefore it is critical to have an idea on both techniques because design teams will often blend these methods.