Monitoring properties

About runtime verification

Like any executable software artefacts, statecharts can and should be tested during their development.

One possible appproach is to test the execution of a statechart by hand, writing unit tests or BDD tests. The Sismic interpreter stores and returns several values that can be inspected during the execution, including the active configuration, the list of entered or exited states, etc. The functional tests in tests/test_interpreter.py on the GitHub repository are several examples of this kind of tests.

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.
• 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 and event attribute.

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