Appendix A AADL Modeling Tutorial
This annex describes how to use AADL to model the architecture and behavior of a simple settable thermostat. The aim of this tutorial is to introduce through an example the main concepts of top-down component-based design in AADL, and to show the specific AADL modeling constructs supported by the VERDICT tool chain.
In the following section, we present a top-level specification for a simplified design of a domestic thermostat system. Then we decompose the thermostat system into subsystems, and show how to represent this hierarchy in AADL. After modeling the architecture, we show how to use the AGREE annex, an assume-guarantee-style dataflow specification language, to describe the behavior of the subcomponents. Finally, we will annotate the top-level system with some formal properties describing the expected behavior of the whole system.
We want to model a thermostat controller for regulating the temperature in a room. The task of the controller is to make sure that the room temperature stays close to the reference temperature set by the user on the thermostat. The figure on the right shows the control panel for the thermostat. It has a switch with three positions (Cool, Off, and Heat), two buttons (Up and Down), and a display that shows at all times the reference temperature, the _set point_. The user can use the switch to place the system in one of the three possible settings, and the two buttons to increase or decrease the desired temperature. The controller can influence the temperature by turning on and off an air conditioning system and a furnace, and it can check the current temperature by reading the value provided by a temperature sensor. When the system is in the Cool setting and the current room temperature (as measured by the sensor) is higher than the set point, the controller sends an activation signal to the air conditioner until the measured temperature goes down to the set point or below. When the system in the Heat setting and the measured temperature is lower than the set point, the controller sends an activation signal to the furnace until that temperature goes up to the set point or above it. To prevent the thermostat from activating the air conditioner or the furnace continually as the room temperature oscillates around the set point, we define a _deadband_, an interval around the set point value, in which neither system will turn on.
The following figure shows the inputs and outputs of the thermostat controller according to the description above:
As a next step in the design, we can conceptually decompose the thermostat controller into two subsystems: component SetDesiredTemperature which keeps track of the reference temperature, and component ControlTemperature which controls the activation signals that turn the air conditioner and the furnace on and off. The interconnections among these subcomponents are shown in the following diagram:
This design can be captured in an AADL model as detailed in the next section.
The architecture of the system, consisting in its component subcomponents and their connections is defined using standard AADL constructs. AADL does not have a native sublanguage for specifying in a formal way the behavior of a component. This can be done, however, with an AADL annex specifically designed for this purpose by Rockwell-Collins: the AGREE annex.
To model an architectural design like this one in AADL one starts by defining each (sub)component and its interface. Each component is defined independently as a system. Here is a possible specification in AADL of ThermostatController, the top-level component in our example, that reflects the first diagram above:
And here is the specification for the ControlTemperature subcomponent:
For each component we list the set of input and output ports that the component uses to communicate with its environment, and the type of data exchanged in each of its port. In addition to base types, such as Boolean, Float and so on, AADL allows one to use user-defined data types for ports. For instance, SwitchPosition is an user-defined enumeration type that models the three possible positions of the thermostat switch:
Once we have defined the interface of the components, we can describe their internal structure. Starting with the top-level component ThermostatController, we do that by defining a system implementation for the component:
The implementation construct allows us to specify the system's subcomponents as well as how they are connected together. In this case, the subcomponents are set_desired_temperature and control_temperature defined respectively as instances of ThermostatController and ControlTemperature. (In terms of object-oriented programming concepts, one can understand systems are classes and subcomponents as class instances).
Once the architectural design is in place, we can describe the behavior of each subcomponent. We do that by associating an assume-guarantee contract to each component. The contract specifies the component's input-output behavior as guarantees provided by the component whenever its environment satisfies certain given assumptions. Intuitively, assumptions describe the expectations the component has on the environment, while guarantees describe restrictions on its output. Assume-guarantee contracts in AGREE are in essence statements in a temporal logic rich enough to describe precisely a component's behavior from the point of view of an observer that, at all times, has access to all the input and output values until so far. Contracts provide a mechanism for capturing the information needed to specify and reason about component-level properties at a desired level of abstraction.
Technical note: The AGREE language is inspired by, and is very close to, the synchronous dataflow language Lustre. In AGREE, every system can be seen as taking as input one or more infinite streams of values (with all values in a stream having the same type), and producing one or more infinite streams as output. The overall system is assumed to run on a universal base clock that represents the smallest time span the system is able to distinguish. Note that the restriction to a synchronous model of computation is intentional, because of its simplicity, but does not cause a loss of generality since asynchronous systems can be faithfully simulated in it in a variety of ways. Our thermostat example can be modeled directly as a synchronous system. The behavior of this system can be formalized by specifying how, at each tick of the base clock, or step, the system's output relates to the current input and past values of the input and output ports as well as the current and past values of local variables (which can be understood as registers).
Let's start with the specification of component SetDesiredTemperature. Recall that this component receives two inputs, up_button and down_button, each of them indicating if the corresponding button is being pressed in the current step, and computes one output, the current value of setpoint. When the user presses the up button, the set point is increased by some fixed amount. We will use a global constant called DIFF to represent such amount. When the user presses the down button, the set point is decreased by the same amount. If neither button is pressed, the set point value doesn't change in that step. More precisely, the set point value changes as long as it stays within a reasonable temperature range, given by a minimum value and a maximum value, denoted respectively by the global constants MIN_TEMPERATURE and MAX_TEMPERATURE. The following AADL snippet shows the interface and AGREE contract specification for SetDesiredTemperature that captures the requirements above:
Each guarantee specifies the current value of setpoint in terms of the auxiliary variable prev_setpoint, which represents the value of setpoint in the previous step. The contract includes the definition of two more auxiliary variables, increment_condition and decrement_condition, that specify the condition under which the setpoint value is to be incremented or decremented.
Auxiliary variables are introduced by eq keyword and are given a name, a type and a definition. The definition of prev_setpoint is given by the combination of the infix initialization operator -> and the delay operator pre. The -> operator can be used to specify the initial value of a port or variable (with the left-hand argument) and later values (with the right-hand argument). An expression of the form e1 -> e2 evaluates to the value of expression e1 initially and to the value of e2 at all later steps of the system's computation. The pre operator is used to refer to the value of an expression in the previous step, if any. That is, at each step i other than the initial one pre(e) denotes the value that e had in step i-1, and is undefined at step 0, the initial step. This means that a pre application should always be guarded by an -> expression, as in the definition of prev_setpoint. That definition specifies that the initial value of prev_setpoint is that of the global constant INITIAL_TEMPERATURE; at each later step it is instead the previous value of setpoint.
Assumptions and guarantees are introduced respectively by the keyword assume and guarantee. They have an optional name, given as a string literal, and a definition. The latter is any expression of (AGREE) type bool which is a synonym of the AADL type Boolean. Expressions of type bool can be built out of ports of type Boolean; auxiliary variables of type bool; relational operators such as =, <, <=, >=, and so on; and various Boolean operators for negation (not), conjunction (and),disjunction (or), , implication (=>), and alternative (if _ then _ else).
Now we will model the behavior of the component ControlTemperature. This component receives as input the position of the switch, the current room temperature, and the current set point, and outputs (as Boolean values) activation signals for the external heating and cooling units. Its behavior can be naturally modeled by describing what the component should do depending on the specific situation, or mode, it is in. Abstractly, we can say that at any one time, the component is in one of three different modes which we represent by three Boolean variables: cool_mode, heat_mode, and off_mode. Each of them is supposed to be true exactly when the thermostat is in the corresponding mode. The cooling (resp., heating) activation signal should be true exactly when controller is in Cool (resp., Heat) mode. Let's consider first the definition of the Cool mode. The component should be in Cool mode in exactly two cases:
-
The current room temperature is outside the deadband region, and the switch is in the Cool position.
-
The current temperature was outside the deadband region in an earlier step, the switch has been in the Cool position since then, and the current temperature is still higher than the set point.
The definition of the Heat mode is analogous. Finally, the component should be in Off mode exactly when it is not in Cool or Heat mode. Intuitively this includes all times the input switch is in the off position but also the times when switched has been most recently moved to one of the other two positions but the current temperature is still within the deadband region. (Recall that we do not want heating or cooling to start until the current temperature is outside that region.)
All requirements are formalized by the following AGREE specification ControlTemperature.
By the definition of the binary operator enum in AGREE, the predicate enum(SwitchPosition, Cool) is true exactly at those times when the value of SwitchPosition is Cool. The values of the other applications of enum are defined analogously.
Note that since we decided to make the definition of the Cool and Heat modes coincide with the cases when the corresponding activation signals are supposed to be true, the definition of those signals becomes trivial and corresponds directly to the values of the Boolean variables cool_mode and heat_mode.
Once we have defined a contract for the subcomponents of the thermostat controller, we can proceed to specify some properties that the controller should satisfy. We will express these properties as a contract for the top-level component ThermostatController. Note that, in the spirit of compositional reasoning enabled by assume-guaranteed contracts, we do not need, and should not need, to know how the two subcomponents are implemented to be able to reason about whether the the top-level component satisfies its contract. In other words, the implementation of ThermostatController and the contracts of SetDesiredTemperature and ControlTemperature, are supposed to be enough to prove the properties of ThermostatController. If they are not, then one of the three contracts or the specification of ThermostatController's implementation needs to be revised. We illustrate this in some detail next, in particular, showing how the results of the analysis provided by VERDICT suggests which part of the behavioral model needs revising when one of the top-level properties is falsified.
We start with four basic properties over the activation signals:
Then we specify four properties over the set point:
Unfortunately, the last two properties don't hold with the current specification. To see why let's consider the last one. This property is violated every time the current value of setpoint is MIN_TEMPERATURE and the up and down input signals are simultaneously true. VERDICT can show this by providing a counterexample trace for the property. The same analysis will show that the increment condition defined in the SetDesiredTemperature contract is satisfied. It must be then the case that setpoint is increased by DIFF. But this violates the property when the down button is also pressed. We can argue about the other property in a similar way. Our first reaction to this should be to double-check the two properties and convince ourselves that we have formalized them correctly. Since this is the case here, we should then ask ourselves whether it is justified to assume that up_button and down_button are never true at the same time given that the problem identified by the analysis occurs when they are both true. If this assumption about the system's environment is justified, we can formalize it by adding the following clause to the specification:
Observe that the assumption talks explicitly about the values of the two inputs being mutually exclusive just in the current step. However, since the current step is arbitrary it effectively expresses a universal restriction on all steps. The same observation applies to guarantees as well.
Finally, we consider these other properties that involve the activation signals, the set point, and the current temperature:
The last two properties use the binary temporal operator Since which is defined so that Since(X,Y) which is true precisely when X has been true at some point, and Y has been continuously true afterwards. AGREE provides a number of temporal operators that facilitate the formalization of assumptions and guarantees. Thanks to the power of the specification language, however, none of them is primitive as it can be defined (basically as a macro) in terms of the operators we have already seen. For instance, here is the definition of Since:
Additional operators, temporal or not, can be defined by the user by providing node definitions like the one above.
The final AADL model for the Thermostat Controller is available here. You can comment out the assumption "Up/Down button signals are mutually exclusive" (by prepending it with --) to verify the failure of the two setpoint properties mentioned earlier.