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 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 a Statechart and a named parameter clock (a Clock instance) 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¶

The complete list of MetaEvent that are created by the interpreter is described in the documentation of the attach() method:

Interpreter.attach(listener)

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 time attribute.
step ended: when a (possibly empty) 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.
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 ard exposed respectively through the source, target and event attributes.
Every meta-event that is sent from within the statechart.

This is a low-level interface for self.bind and self.bind_property_statechart.

Consult sismic.interpreter.listener for common listeners/wrappers.

Parameters:: listener (Callable[[MetaEvent], Any]) – A callable that accepts meta-event instances.
Return type:: None

Note

Property statecharts are not the only way to listen to these meta-events. Any listener that is attached with attach() will receive these meta-events.

Property statecharts can listen to what happens in an interpreter when they are bound to this interpreter, using bind_property_statechart() method:

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 attach method 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 PropertyStatechartError will 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 self.attach. If x = interpreter.bind_property_statechart(...), use interpreter.detach(x) to unbind a previously bound property statechart.

Parameters:

statechart (Statechart) – A statechart instance.
interpreter_klass (Callable) – An optional callable that accepts a statechart as first parameter and a named parameter clock. Default to Interpreter.

Return type:

Callable[[MetaEvent], Any]

Returns:

the resulting attached listener.

Internally, this method wraps given property statechart to an appropriate listener, and calls 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 bind_property_statechart().

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.