Behavioral Modeling - Power Window

This example demonstrates modeling both structure and behaviour with variability.

Module Downloads: | [.cfr] | [.html] |

Feature modeling

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.


abstract final Feature
abstract final FeatureModel


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.

WinFeatures : FeatureModel
manualUpDown : Feature
express : Feature ?
pinchProtection : Feature ?

Component and statemachine modeling


Simple component modeling. Nesting the Port under 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.

abstract final Component
abstract Port
abstract final Command

Inside the components, we will embed statemachines modeling their behavior. The states are not final because we want to allow state changes.

abstract State
abstract final StateMachine


Commands received by the window motor.

motorUp : Command
motorStop : Command
motorDown : Command

Window motor. The port cmd is mandatory, meaning that the motor must always be given a command.

abstract WinMotor : Component
cmd : Port -> Command

Requests from the user. Observe, that the request expressUp is optional.

abstract final UserRequest
expressUp : UserRequest ?
stop : UserRequest
down : UserRequest

The user request expressUp is only available when the feature express is present (alphabet variability).

The component pinchDetector of the WinController is only required if the feature pinchProtection is present.

Instances of the ports endOfTravel and 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 req, endOfTravel, and objectDetected in order to remove non-determinism.

abstract WinController : Component
motor : WinMotor
pinchDetector : Component ?
req : Port -> UserRequest ?
endOfTravel : Port ?
objectDetected : Port ?
[ always req = stop between req = down and req = up ]
[ always req = stop between req = up and req = down ]
[ always req = up between req = stop and req = expressUp ]
[ always req = expressUp => next no req ]
final xor WinStates : StateMachine
xor movingUp : State
[ req = down --> movingDown ]
[ req = up --> movingUp ]
initial basic : State
[ req = stop --> stopped ]
movingUpX : State
[ this -[objectDetected]--> stopped ]
initial xor stopped : State
closed : State
[ req = down --> movingDown ]
[ req = up || req = stop --> closed ]
partlyOpen : State
[ req = up --> movingUp ]
[ req = down --> movingDown ]
[ req = stop --> partlyOpen ]
open : State
[ req = up --> movingUp ]
[ req = down || req = stop --> open ]
movingDown : State
[ req = up --> movingUp ]
[ endOfTravel --> open ]
[ req = stop --> stopped ]
[ req = down --> movingDown ]

We model state actions by fixing the motor command. E.g., in state movingDown, motor command is fixed to motorDown.

State transitions are modeled using “next transitions”: -->. In the state movingUpX we demonstrate “guarded next transition”: -[objectDetected]->.

Disabling objectDetected port

Without the feature pinchProtection, the port objectDetected should be inactive. Having the feature will allow receiving the signal objectDetected.

Variability in behavior using inheritance

Two kinds of window controllers:

With continuous chime

WinCtrWithContChime : WinController ?
chime : Port ?
[ movingUpX <=> chime ]

With intermittent chime

WinCtrWithChime : WinController ?
chime : Port ?
[ no movingUpX => no chime ]
[ chime --> no chime ]
[ no chime && movingUpX --> movingUpX => 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).

abstract ChimingStrategy
active : State ?
audible : State ?

Concrete strategies:

NoChiming : ChimingStrategy
[ not audible ]
Continuous : ChimingStrategy
[ active => audible ]
Intermittent : ChimingStrategy
[ audible --> not audible ]
[ not audible --> active => audible ]

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.

WinControllerStrategies : WinController ?
chime : Port ?
strategy -> ChimingStrategy

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

assert [ never wc3.req = down --> wc3.WinStates.stopped.closed ]

It must be impossible for the window to be closed and continue sending motorUp command

It is a safety property to prevent burning the motor.

assert [ never wc4.WinStates.stopped.closed && wc4.motor.cmd = motorUp ]

The window must never continue movingUp after an object was detected

It is a safety property to prevent injury.

assert [ never wc5.objectDetected --> wc5.WinStates.movingUp ]