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 a
Statechart instance that is used to create an interpreter for
the property statechart. This method also accepts an optional
interpreter_klass parameter as a callable accepting
Statechart and a named parameter
and is used to build an interpreter for the property statechart.
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¶
Attach given listener to the current interpreter.
The listener is called each time a meta-event is emitted by current interpreter. Emitted meta-events are:
step started: when a (possibly empty) macro step starts. The current time of the step is available through the
step ended: when a (possibly empty) macro step ends.
event consumed: when an event is consumed. The consumed event is exposed through the
event sent: when an event is sent. The sent event is exposed through the
state exited: when a state is exited. The exited state is exposed through the
state entered: when a state is entered. The entered state is exposed through the
transition processed: when a transition is processed. The source state, target state and the event ard exposed respectively through the
Every meta-event that is sent from within the statechart.
This is a low-level interface for
sismic.interpreter.listenerfor common listeners/wrappers.
Property statecharts are not the only way to listen to these meta-events. Any listener
that is attached with
attach() will receive these
Property statecharts can listen to what happens in an interpreter when they are bound to
this interpreter, using
- Interpreter.bind_property_statechart(statechart, *, interpreter_klass=None)
Bind a property statechart to the current interpreter.
A property statechart receives meta-events from the current interpreter depending on what happens. See
attachmethod for a full list of meta-events.
The internal clock of all property statecharts is synced with the one of the current interpreter. As soon as a property statechart reaches a final state, a
PropertyStatechartErrorwill be raised, meaning that the property expressed by the corresponding property statechart is not satisfied. Property statecharts are automatically executed when they are bound to an interpreter.
Since Sismic 1.4.0: passing an interpreter as first argument is deprecated.
This method is a higher-level interface for
x = interpreter.bind_property_statechart(...), use
interpreter.detach(x)to unbind a previously bound property statechart.
Internally, this method wraps given property statechart to an appropriate listener, and
attach() so you don’t have to.
Bound property statecharts can be unbound from the interpreter by calling the
detach() method. This method accepts a
previously attached listener, so you’ll need to keep track of the listener returned
by the initial call to
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.