SpeQTr Cookbook

This document provides a set of specifications that cover some common features and use cases of the SpeQTr language. You can use these as starting points for constructing your own specifications. Since queries are basically event patterns you can also use the event patterns in these example specifications as inspiration for writing your own queries.

# Check for Specific Failure Event

This specification checks that a specific failure event never occurs.

behavior "No failures"
    prohibited case "Catastrophic failure"
        catastrophic_failure@commander
    end
end

# No Critical Failures

This specification checks that there are no events with severity higher than level 6, which we consider to be critical failures. You could write similar specifications using any other event or timeline attributes.

behavior "No high severity events"
    prohibited case "Severity above 6"
        *@*(_.severity > 6)
    end
end

# Metadata

This example shows how you can add metadata attributes to various levels of a specification. The metadata key names used here are just examples - you can use whatever keys you want to fit your process or application.

# @author = "phil"
# @project = "documentation"

# @type = "example"
behavior "Example behavior"
    when "A message is sent"
        sent_message@worker AS sent
    end

    # @requirement_id = 3
    nominal case "The message is received"
        sent FOLLOWED BY received_message@monitor
    end

    # @requirement_id = 7
    # @category = "remediation"
    recovery case "Message retry"
        sent FOLLOWED BY retry_message@worker FOLLOWED BY received_message@monitor
    end

    # @requirement_id = 9
    # @category = "failure"
    prohibited case "Connection lost"
        connection_lost@monitor
    end
end

# Event attribute stays within bounds

This specification checks that a certain event's attribute was never outside the appropriate bounds.

behavior "Voltage within bounds"
    prohibited case "Voltage is outside permitted range"
        filtered_voltage@battery(_.voltage < 11.5 OR _.voltage > 12.3)
    end
end

# Event attribute stays above threshold

This specification is similar in structure to the one above except that it only checks an upper bound. The other notable aspect here is the fact that, for this specification, we have instrumented our simulator, allowing us to check values that it reports as well.

behavior "Maximum velocity"
    prohibited case "Velocity above maximum bound"
        ground_truth_velocity@simulator(_.velocity > 300)
    end
end

# Check Pattern Across Subsystems

This specification checks that a certain pattern always occurs as expected, specifically that every time the land detection subsystem detects takeoff the commander subsystem registers it. We have bounded the case evaluation by requiring it to occur before any subsequent takeoff_detected event.

behavior "Takeoff detection"
    when "Land detector takeoff"
        takeoff_detected@land_detector as LandDetectorTakeoff
    end

    until "Subsequent takeoff event"
        takeoff_detected@land_detector
    end

    nominal case "Commander takeoff detected"
        LandDetectorTakeoff FOLLOWED BY takeoff@commander
    end
end

# Check Time-Sensitive Pattern

This specification checks that the system's pre-flight checks complete successfully within the required amount of time. It verifies both the timing aspect and that the checks were successful (with the event attributes). See the note in the section on time-limited relationships for requirements for time-based specifications.

behavior "Preflight checks"
    when "Preflight checks begin"
        sensors_preflight_check@commander(_.action = "begin") AS CheckSensors
    end

    nominal case "Checks pass within 100ms"
        CheckSensors FOLLOWED BY WITHIN 100ms preflight_check_complete@commander(_.success = true)
    end
end

# Check Time-Sensitive Multi-Event Pattern

This specification checks that gyroscope-based failure detection always proceeds as expected. Specifically, every gyroscope reading should be reported within 100 milliseconds, and a multi-timeline sequence of events ending at the failure detector should be observed. This example demonstrates the use of recovery case to specify correct remediation behavior alongside nominal behavior.

behavior "Gyroscope informs failure detection"
    when "A gyroscope reading is taken"
        *@gyroscope(_.name = "x_axis" OR _.name = "y_axis") AS GyroscopeReading
    end

    until "Next gyroscope reading is taken"
        *@gyroscope(_.name = "x_axis" OR _.name = "y_axis") 
    end

    nominal case "Gyroscope reading flows to failure detector within 100ms"
        GyroscopeReading FOLLOWED BY
        sample_reported@gyroscope AS GyroscopeReport FOLLOWED BY
        sensors_polled@sensors FOLLOWED BY
        failure_detector_updated@commander as Detected
        AND GyroscopeReading FOLLOWED BY WITHIN 100ms Detected
    end

    recovery case "Gyroscope report requires a retry"
        GyroscopeReport FOLLOWED BY
        sample_report_retry@gyroscope FOLLOWED BY
        sensors_polled@sensors FOLLOWED BY
        failure_detector_updated@commander
    end
end

# Aggregate in a Specification

This specification checks some statistical properties of the given event's attributes.

behavior "Gyroscope x axis distribution"
    nominal case "Gyroscope x axis mean and stddev within tolerance"
        x_axis@gyroscope AS x
        AGGREGATE
            -10.0 < mean(x.acceleration) < 10.0
            AND std_dev(x.acceleration) < 2.1
    end
end

# Negative Lookahead

This specification shows another way to write the check pattern across subsystems example above, using the negative lookahead operator. Where the example above says that a certain event should always be followed by another one, this specification says that we should never see the first event without then seeing the second event.

behavior "Takeoff detection"
    prohibited case "Commander takeoff not detected"
        takeoff_detected@land_detector NOT FOLLOWED BY takeoff@commander
    end
end

# Check Absence of Event On Path

This specification checks that there is a path from mission startup to mission end that does not have any events with the "failure" tag on it. We use a negative path constraint to express this.

behavior "Full mission without failure"
    when "Mission starts"
        mission_start@commander AS MissionStart
    end

    nominal case "Mission ends without any failures occurring"
        MissionStart NOT FOLLOWED BY *@*(_.tag = "failure") FOLLOWED BY mission_end@commander
    end
end

# Check Events Have Same Attribute Value

This specification checks that every velocity reading is acknowledged by the commander subsystem with an event that has the same attribute value.

behavior "Velocity readings acknowledgment"
    when "A velocity reading is taken by the sensor"
        velocity_reading@sensors AS SensorVelocity
    end

    nominal case "The commander receives the correct velocity reading"
        SensorVelocity FOLLOWED BY velocity_received@commander AS CommanderVelocity AND
        SensorVelocity.velocity = CommanderVelocity.velocity
    end
end

← Syntax