Overview of SpeAR - lgwagner/SpeAR GitHub Wiki

SpeAR captures requirements in a formal language that not only provides the semantics of Past LTL^[1], but is also designed to read like natural language. SpeAR v2.0 provides English alternatives for most operators, such as equal to, greater than, less than or equal to, implies, and not. Additionally, SpeAR provides aliases for many operators so that systems engineers can more naturally express their requirements.

Table of Contents Thermostat Example Inputs, Outputs, State Assumptions Requirements Properties References

We motivate further discussion of the SpeAR language by describing partial requirements for the thermostat of a simple heating system. As seen in Figure 1a, the thermostat is represented by a three-state automaton describing reactions to changes in the ambient temperature.

SpeAR promotes grouping requirements according to system components enabling modularity and reuse. Requirements are captured in files laid out in a common structure. Partial requirements for the thermostat, a component of the heating system, are shown in Figure 1b.

Inputs represent monitored or observed data from the environment, as well as inputs from other components. Outputs represent data to the environment, as well as outputs to other components. State represents data that is not visible to the environment or to other components. For example, the thermostat monitors the ambient and target temperatures for a room (inputs), controls the heater by sending a signal that turns it on or off (outputs), and has a counter that tracks heating duration (state).

Assumptions identify necessary constraints on inputs from the environment and from other components. For example, the thermostat assumes that the ambient temperature rises when the heater is on (a0). This constraint is an assumption: the thermostat cannot directly control the ambient temperature.

Requirements identify constraints that the component must guarantee through its implementation. For example, the thermostat will send a signal to turn the heater on when the ambient temperature is lower than the target temperature (r0).

Properties represent constraints that the system should satisfy when operating in its intended environment. Properties can be used to validate that the requirements define the correct component behavior or to prove that certain undesirable conditions never arise. For example, the heater is only on when the ambient temperature is below the target temperature (p_heat).

1. ^ Cimatti, A., Roveri, M., Sheridan, D.: Bounded Verification of Past LTL, pp. 245-259. Springer Berlin Heidelberg (2004)