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.
# @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
# Check an Event's Payload
This specification checks that a certain event's payload was never outside the appropriate bounds. In addition, it gives an example of adding metadata to specifications, for both the behavior and the case.
behavior "Voltage within bounds"
prohibited case "Voltage is outside permitted range"
filtered_voltage@battery(_.payload < 11.5 OR _.payload > 12.3)
end
end
# Check Simulator Value
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(_.payload > 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.
behavior "Takeoff detection"
when "Land detector takeoff"
takeoff_detected@land_detector as LandDetectorTakeoff
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
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
# Check Payload Aggregate
This specification checks some statistical properties of the given event's payload.
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.payload) < 10.0
AND std_dev(x.payload) < 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 Payload
This specification checks that every velocity reading is acknowledged by the commander subsystem with an event that has the same payload.
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.payload = CommanderVelocity.payload
end
end
← Syntax