Monitoring properties¶
About runtime verification¶
Another key feature of Sismic’s interpreter is its support for monitoring properties at runtime, not only contracts. To avoid a statechart designer needing to learn a different language for expressing such properties, these properties are expressed using the statechart notation. These properties are then called property statecharts
Using statecharts to express properties¶
Property statecharts can be used to express functional properties of the intended behaviour in terms of the events that are consumed or sent, or in terms of the states that are entered or exited by a statechart. When a statechart is executed by Sismic, specific meta-events are created based on the events that are sent or consumed, the states that are entered of exited, etc. When the statechart being monitored is executed, the meta-events are propagated to all associated property statecharts. The property statecharts will look for property violations based on those meta-events, following a fail fast approach: they will report a failure as soon as the monitored behavior leads to a final state of the property statechart.
Due to the meta-events being considered and the “fail-fast” approach adopted by Sismic for their verification, property statecharts are mainly intended to check for the presence of undesirable behavior (safety properties), i.e., properties that can be checked on a (finite) prefix of a (possibly infinite) execution trace. While it is technically possible to use property statecharts to express liveliness properties (something desirable eventually happens), this would require additional code for their verification since liveliness properties are not supported “as is” by Sismic.
During the execution of a statechart, several meta-events are created depending on what happens in the statechart being executed. Those meta-events are automatically send to any previously bound property statechart.
To bind a property statechart to an interpreter, it suffices to provide the property statechart as a
parameter of the bind_property_statechart()
method of an interpreter.
This method accepts either a Statechart
or an Interpreter
instance.
When a property statechart is bound to an interpreter, its internal clock (the
time
attribute) is automatically synchronised with the one of the
interpreter.
If a property statechart reaches a final state during its execution, then the property is considered as not
satisfied, and a PropertyStatechartError
is raised.
This exception provides access to the interpreter that executed the property, the active configuration of statechart
being executed, the latest executed MacroStep
and the current context of the interpreter.
Meta-events generated by the interpreter¶
The complete list of MetaEvent
that are created by the interpreter is described in the
documentation of the bind_property_statechart()
method:
-
Interpreter.
bind_property_statechart
(statechart_or_interpreter) Bind a property statechart to the current interpreter. A property statechart receives meta-events from the current interpreter depending on what happens:
- step started: when a macro step starts.
- step ended: when a macro step ends.
- event consumed: when an event is consumed. The consumed event is exposed through the
event
attribute. - event sent: when an event is sent. The sent event is exposed through the
event
attribute. - delayed event sent: when a delayed event is sent. The sent event is exposed through the
event
attribute. - state exited: when a state is exited. The exited state is exposed through the
state
attribute. - state entered: when a state is entered. The entered state is exposed through the
state
attribute. - transition processed: when a transition is processed. The source state, target state and the event are
exposed respectively through the
source
,target
andevent
attribute.
Additionally, MetaEvent instances that are sent from within the statechart are directly passed to all bound property statecharts. This allows more advanced communication and synchronisation patterns with the bound property statecharts.
The internal clock of all property statecharts will be synced with the one of the current interpreter. As soon as a property statechart reaches a final state, a
PropertyStatechartError
will be raised, implicitly meaning that the property expressed by the corresponding property statechart is not satisfied.Parameters: statechart_or_interpreter ( Union
[Statechart
,Interpreter
]) – A property statechart or an interpreter of a property statechart.Return type: None
Examples of property statecharts¶
7th floor is never reached¶
This property statechart ensures that the 7th floor is never reached. It stores the current floor based on the number of times the elevator goes up and goes down.
statechart:
name: Test that the elevator never reachs 7th floor
preamble: floor = 0
root state:
name: root
initial: standing
states:
- name: standing
transitions:
- event: state entered
guard: event.state == 'moving'
target: moving
- guard: floor == 7
target: fail
- name: moving
transitions:
- event: state entered
guard: event.state == 'movingUp'
action: floor += 1
- event: state entered
guard: event.state == 'movingDown'
action: floor -= 1
- event: state exited
guard: event.state == 'moving'
target: standing
- name: fail
type: final
Elevator moves after 10 seconds¶
This property statechart checks that the elevator automatically moves after some idle time if it is not on the ground floor. The test sets a timeout of 12 seconds, but it should work for any number strictly greater than 10 seconds.
statechart:
name: Test that the elevator goes to ground floor after 10 seconds (timeout set to 12 seconds)
preamble: floor = 0
root state:
name: root
initial: active
states:
- name: active
parallel states:
- name: guess floor
transitions:
- event: state entered
guard: event.state == 'movingUp'
action: floor += 1
- event: state entered
guard: event.state == 'movingDown'
action: floor -= 1
- name: check timeout
initial: standing
states:
- name: standing
transitions:
- event: state entered
guard: event.state == 'moving'
target: moving
- guard: after(12) and floor != 0
target: timeout
- name: moving
transitions:
- event: state exited
guard: event.state == 'moving'
target: standing
- name: timeout
type: final
Heating does not start if door is opened¶
This property statechart checks that the heating of a microwave could not start if the door is currently opened.
statechart:
name: Heating does not start if door is opened
root state:
name: root
initial: door is closed
states:
- name: door is closed
transitions:
- target: door is opened
event: event consumed
guard: event.event.name == 'door_opened'
- name: door is opened
transitions:
- target: door is closed
event: event consumed
guard: event.event.name == 'door_closed'
- target: failure
event: event sent
guard: event.event.name == 'heating_on'
- name: failure
type: final
Heating must stop when door is opened¶
This property statechart ensures that the heating should quickly stop when the door is open while cooking occurs.
statechart:
name: Test that the elevator never reachs 7th floor
preamble: floor = 0
root state:
name: root
initial: standing
states:
- name: standing
transitions:
- event: state entered
guard: event.state == 'moving'
target: moving
- guard: floor == 7
target: fail
- name: moving
transitions:
- event: state entered
guard: event.state == 'movingUp'
action: floor += 1
- event: state entered
guard: event.state == 'movingDown'
action: floor -= 1
- event: state exited
guard: event.state == 'moving'
target: standing
- name: fail
type: final