Revision 60b85fe10793879b2f357c5173c2e858d57ea221 (click the page title to view the current version)

Behavioral Modeling - Power Window

Modeling variability and structures with variability

Feature modeling

Metamodel

abstract final Feature
abstract final FeatureModel

Model

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

Structural modeling

Metamodel

abstract final Component
abstract Port
abstract final Command
abstract State
abstract StateMachine

Model

Commands and requests.

motorUp : Command
motorStop : Command
motorDown : Command
abstract final UserRequest
expressUp : UserRequest ?
stop : UserRequest
down : UserRequest

Window motor

WinMotor : Component
cmd : Port -> Command

Window controller

abstract WinController : Component
final motor -> WinMotor
pinchDetector : Component ?
req : Port -> UserRequest ?
endOfTravel : Port ?
objectDetected : Port ?
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 ]

Variability in structural models

Linking the feature with the optional component (structural variability)

The component pinchDetector is only required if we support the feature pinchProtection.

Disabling objectDetected port

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

Alphabet variability

The user request expressUp is only available when the feature express is present.

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 Behavior 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 parameterize 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

An example positive scenario

assert [ initially closed && req = down --> movingDown -->> req = expressUp --> movingUpX --> objectDetected --> stopped ]

It must be possible to go from closed to open via partiallyOpen state

assert [ sometime closed -->> partlyOpen -->> open ]

It must be impossible for the user to request opening and the window remains closed

assert [ never req = down --> 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 closed && cmd = motorUp ]

The window must never continue movingUp after an object was detected

It is a safety property to prevent injury.

assert [ never objectDetected --> movingUp ]