- Feature modeling
- Component and statemachine modeling
- Variability in behavior using inheritance
- Variability in behaviour using strategy pattern
- Scenarios and properties
- An example positive scenario
- It must be possible to go from closed to open via partiallyOpen state
- It must be impossible for the user to request opening and the window remains closed
- It must be impossible for the window to be
closedand continue sending
- The window must never continue
movingUpafter an object was detected
This example demonstrates modeling both structure and behaviour with variability.
We model features as final, that is, we do not allow dynamic reconfiguration. Feature configuration from the first snapshot remains unchanged for the entire trace.
The optional feature
express indicates the functionality of automatically closing the window. The feature
pinchProtection indicates the functionality of detecting obstacles and stopping the window.
Component and statemachine modeling
Simple component modeling. Nesting the
Component ensures that all ports are always children of components. The components are final because we do not allow dynamic reconfiguration; however, the ports are not final: a port instance can appear to point to a value, disappear, and a new instance can appear to point to a different value.
Inside the components, we will embed statemachines modeling their behavior. The states are not final because we want to allow state changes.
Commands received by the window motor.
Window motor. The port
cmd is mandatory, meaning that the motor must always be given a command.
Requests from the user. Observe, that the request
expressUp is optional.
The user request
expressUp is only available when the feature
express is present (alphabet variability).
pinchDetector of the
WinController is only required if the feature
pinchProtection is present.
Instances of the ports
objectDetected appear when the corresponding binary signal is received. On the other hand, instances of the port
req point to a specific user request. No instance of the port
req indicates no user request. Finally, we allow at most one of
objectDetected in order to remove non-determinism.
We model state actions by fixing the motor command. E.g., in state
movingDown, motor command is fixed to
State transitions are modeled using “next transitions”:
-->. In the state
movingUpX we demonstrate “guarded next transition”:
Without the feature
pinchProtection, the port
objectDetected should be inactive. Having the feature will allow receiving the signal
Variability in behavior using inheritance
Two kinds of window controllers:
With continuous chime
With intermittent chime
Variability in behaviour using strategy pattern
We first define an abstract chiming strategy: chiming can be
audible but only if
active (expressed by nesting).
Now we can parametrize the controller with a chiming strategy. Chiming should be active when moving up in express mode. The chime should be emitted only when the chiming is audible.
We can choose the chiming strategy using the following constraint:
Scenarios and properties
For each case, we define a concrete WinController and state the assertion.
An example positive scenario
It must be possible to go from closed to open via partiallyOpen state
It must be impossible for the user to request opening and the window remains closed
It must be impossible for the window to be
closed and continue sending
It is a safety property to prevent burning the motor.
The window must never continue
movingUp after an object was detected
It is a safety property to prevent injury.