Introduction
The Auxon Specification and Query Trace Language (SpeQTr) is a powerful tool for interacting with your collected data.
# Specs and Queries
The SpeQTr language has two main use cases.
Specifications let you describe the expected behavior of a system composed of multiple interacting components. You can specify both local behavior and interactions which span multiple components. Auxon Conform can then check your specifications over any region of recorded history, telling you whether your system behaves as expected and, when it doesn't, helping you figure out why.
Queries let you directly interact with system trace data acquired with Auxon Modality. A query consists of a small pattern, with one more trace events. Running the query will return a list of all portions of the trace which match the pattern. You can also compute a variety of aggregations over selected parts of the trace.
# What's in a Trace?
In Modality (opens new window), a system trace consists of a collection of timelines. Each timeline is simply a list of events in order. Timelines represent something in your system which is doing things sequentially; a timeline could be a thread in a desktop application, a microprocessor in an embedded system, or a single drone in a fleet, to name a few examples. Trace data is stored in the Modality database, which can evaluate queries over it. Conform (opens new window) uses the data stored in Modality to evaluate specifications, and Deviant (opens new window) lets you go further and inject mutations into your running system.
Causality is central to Modality's tracing system - it's how Modality can tell if one event is before or after another. Unlike other systems you may be used to, event ordering in Modality is not derived from a common time source (unless you specifically say it should be). Instead, Modality relies on the fact that events on a timeline are ordered, along with structured interactions between the timelines, to establish before-and-after relationships between events on different timelines. This means that event ordering in Modality is partial: given two events, one may be before or after the other, or they may have no known ordering at all (that is, they are logically concurrent).
This causal ordering is the backbone of the SpeQTr Language. Modality stores all the collected trace data in a causal graph, where each node is an event, and each edge represents a causal (happened-before, happened-after) relationship between the events. You can inspect this graph directly using the modality log command. (opens new window)
# What's a Specification?
Conform specifications give you a way to use Modality's causal graph to check things about your system. The conform spec eval (opens new window) command evaluates specifications over specific regions of observed behavior, and specifications are said to pass if the system behavior matches the specification. When appropriate, Conform can help you narrow down which parts of a failing specification are being violated and suggest values that could make the specification pass.
You might use a specification to:
- Assert that all values logged at a particular point in your software fall within a certain desired range.
- Assert that all the faults of a certain type are followed by an automatic remediation.
- Assert that some error conditions should never happen.
- Assert that a complex, multi-component initialization sequence always occurs as specified.
# Basic Specification Example
Here is an example of a specification:
behavior "Radar initialization"
when "The radar turns on"
radar_on@control AS radar_on
end
nominal case "A valid reading is received within 250ms"
radar_on FOLLOWED BY WITHIN 250 ms radar_reading@radar(11.7 <= _.supply_voltage <= 13.8 )
end
end
In English, you might describe this as:
Plain english description:
Every time the radar turns on, there should be a reading logged within 250 milliseconds, with a reported supply volatge between 11.7 and 13.8V.
This behavior would fail if there is no radar reading at all, if it occurred too late, or if it reported an out-of-bounds supply voltage.
For more details about writing specifications see the syntax reference. For examples of common specifications see the cookbook.
# What's a Query?
Modality queries let you interrogate your collected trace data. The modality query (opens new window) command takes a query and returns all the places in the system trace that match it. This can be an invaluable tool in investigating bugs, showing you where to start looking or telling you how many times a certain pattern occurred. You can also use queries to perform aggregate calculations over matched events.
Query features:
- Match by event and timeline name/ID, or use wildcards.
- Filter matches with a variety of operators on any event or timeline attribute.
- Describe causal relationships between events, i.e. "event1 FOLLOWED BY event2".
- Calculate aggregate statistics over matched events.
# Basic Query Example
Here is an example of a query:
*@producer AS first FOLLOWED BY *@consumer AS second AND first.sample = second.sample
In English, you might describe this as:
Plain english description:
Look for pairs of events where an event on the producer timeline is followed by an event on the consumer timeline with the same sample value.
Running the above query gives the following results (truncated):
$ modality query '*@* as a -> *@* as b'
Result 1:
═════════
■ init @ power_subsystem [%01f8a1ca53a04854a50879beb4aa194b:01]
║ name = init
║ sim.timestamp = 1969-12-31 16:00:00 -08:00
║ system.timestamp = 2023-09-07 15:47:06.260700578 -07:00
║ timestamp = 1969-12-31 16:00:00 -08:00
║ modality.query.label = a
║
■ get_status @ power_subsystem [%01f8a1ca53a04854a50879beb4aa194b:02]
║ interaction.remote_nonce = 3928169896025843929
║ interaction.remote_timeline_id = %0d5b355952a440f28acabfa2005a83fa
║ name = get_status
║ sim.timestamp = 1969-12-31 16:00:00 -08:00
║ system.timestamp = 2023-09-07 15:47:06.628477038 -07:00
║ timestamp = 2022-12-31 17:01:20.100 -08:00
║ modality.query.label = b
║
Result 2:
═════════
■ init @ power_subsystem [%01f8a1ca53a04854a50879beb4aa194b:01]
║ name = init
║ sim.timestamp = 1969-12-31 16:00:00 -08:00
║ system.timestamp = 2023-09-07 15:47:06.260700578 -07:00
║ timestamp = 1969-12-31 16:00:00 -08:00
║ modality.query.label = a
║
║ ■ power_status @ cpu [%0d5b355952a440f28acabfa2005a83fa:08]
║ ║ interaction.remote_nonce = 6618335283334878753
║ ║ interaction.remote_timeline_id = %01f8a1ca53a04854a50879beb4aa194b
║ ║ name = power_status
║ ║ power.battery_charge = 40
║ ║ power.battery_charge_ratio = 1
║ ║ power.error.out_of_sync = false
║ ║ power.solar_panel_illumination = 0.825
║ ║ sim.timestamp = 1969-12-31 16:00:00 -08:00
║ ║ system.timestamp = 2023-09-07 15:47:06.630704249 -07:00
║ ║ timestamp = 2022-12-31 17:01:20.200 -08:00
║ ║ modality.query.label = b
║ ║
Let's briefly explain the output above. Looking at result 1, we see:
- On the left side is an ASCII art depiction of the matched events, on timelines.
- Matched events are shown with the label they were assigned as the
query.labelattribute, e.g.firstandsecond. - Each matched event displays
<event name> @ <timeline name> [<coordinates>]. Event coordinates constitute a unique ID for a specific occurrence of an event. - Beneath the event and timeline name we see that event's attributes. This example shows the set of attributes Modality displays for these events by default, but you can control which attributes are printed with command line options.
For more details about writing queries see the syntax reference. For examples of common queries see the cookbook.
# SpeQTr is made by the team at Auxon
If you'd like to start a discussion or schedule a demo, contact us. (opens new window)
Syntax →