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
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
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