# How to Validate System Requirements with Modality
Modality lets you describe your system requirements as queries, and then automatically test those queries against recordings of your system in action.
# Compared to Traditional Validation
Validating your system with traditional test methods is a stop-and-go parade of manually inducing behavior, stopping to verify conditions, and repeating for every stage of execution. Modality records all of your system execution without interruption, skipping past the stop-and-go entirely.
Traditional test methods require that a large portion of development time is spent reworking interfaces to make your system testable. Modality can be instrumented deeply so you maintain high visibility throughout development.
Traditionally-written tests are brittle, with narrow parameters that demand constant maintenance to keep them system-accurate. Modality tests are written as flexible queries that describe system behavior, which makes them easy to update alongside troubleshooting or development.
Traditionally, there are several layers of abstraction between system requirements and the code that actually tests them, which makes updating requirements cumbersome. Because the same human-readable Modality query can both specify system requirements and test them, updating requirements is easy.
Traditional integration tests tend to return pass/fail results that provide little guidance to the actual cause of a failure. No matter how complex the system, Modality queries return counterexamples that point to specific events around a test failure.
# Step 1: Write Your System Requirement Test Query
For this first step, we'll use a Modality query to describe one of your system requirements. Modality's flexible query language lets you check system behaviors of any complexity and any specificity.
# 0. Naturally, we're assuming that your team has already instrumented your system with Modality.
For embedded engineers, this is about as easy as integrating any other embedded logging library.
Don't worry, Modality lets TestOps engineers and developers write and run accurate system requirement validation tests without any embedded expertise.
# 1. Open the editor of your choice and create a blank text file.
This will be
<test-query-file.tq>in future steps.
The file extension for this file doesn't matter: we use
.tqin these examples.
# 2. If you want to add a comment to describe your system requirement in natural language, insert
# at the start of a line.
# Req: Velocity shall never exceed the specified value (300 m/s).
# 3. Use Modality's query language to describe your system requirement in terms of system events.
Describe the way your system shall work, either positively in terms of events that do happen, or negatively in terms of conditions that shall never occur.
If you're new to Modality, consider copy-pasting one of the example requirement test queries below, and then adjust to your system's details.
# Req: Velocity shall never exceed the specified value (300 m/s). NEVER GROUND_TRUTH_VEL_UP@GAZEBO_SIMULATOR(_.payload > 300)
# 4. Consider using an example requirement test query.
Optionally, use one of these common use cases to start your own system requirement test query. You can always write your own using the Modality query language instead.
Example: A specific event never happens
- If you have a warning or failure event instrumented into your system, simply assert that it shall never happen.
# Case: A specific event never occurs. # Req: "The command module never reports that arming was denied." # Ex: Event ARMING_DENIED_NOT_LANDED is never seen happening # at the PX4_COMMANDER probe. NEVER ARMING_DENIED_NOT_LANDED@PX4_COMMANDER
Example: An event payload value always stays within bounds
- If you need each instance of an event to stay within a range, verify its payload with a simple operator like
# Case: A payload value stays within bounds. # Req: "Battery voltage always stays within an acceptable range." # Ex: For every FILTERED_VOLTAGE event at the PX4_BATTERY probe, # label it as "filteredVoltage" and verify that its payload value # is between 11.5 and 12.3 FOR EACH FILTERED_VOLTAGE@PX4_BATTERY AS filteredVoltage VERIFY 11.5 <= filteredVoltage.payload <= 12.3
- If you need each instance of an event to stay within a range, verify its payload with a simple operator like
Example: In aggregate, payload values stay within statistical bounds
- If you need to inspect many events collectively, use aggregate functions](../reference/spec-lang.md#aggregate-functions) to evaluate mathematical properties like min, max, mean, count, sum, and standard deviation.
# Case: In aggregate, payload values stay within statistical bounds # Req: "Both the average and standard deviation # of all voltage measurements are nominal." # Ex: For the aggregate of all FILTERED_VOLTAGE events at probe # PX4_BATTERY, verify that the mean of their payload value is between # 12.0 and 13.0, and the payload standard deviation is below 2.1. FOR AGGREGATE FILTERED_VOLTAGE@PX4_BATTERY AS filteredVoltage VERIFY 12.0 < mean(filteredVoltage.payload) < 13.0 AND stddev(filteredVoltage.payload) < 2.1
Example: Events from one component are followed by an event from a different component
- Events from different subsystems can easily be observed by querying events at their probes.
# Case: Events from one subsystem are followed by events # from a different subsystem # Req: "If the land detector subsystem observes take-off, # the command module always recieves notice." # Ex: For each TAKE_OFF_DETECTED event at the PX4_LAND_DETECTOR probe, # label that event "landDetectorTakeoff" and verify that it # was followed by a TAKEOFF_DETECTED event at the PX4_COMMANDER probe FOR EACH TAKE_OFF_DETECTED@PX4_LAND_DETECTOR AS landDetectorTakeoff VERIFY landDetectorTakeoff -> TAKEOFF_DETECTED@PX4_COMMANDER
Example: No failing expectation events
- Expectations are simple events with pass/fail outcomes that can be instrumented into your system. If all of the expectations in your system represent critical failures, you can simply assert that none of them shall fail.
- The two
*in this example are each wildcards, so
*@*means "any event at any probe."
# Case: No expectation events fail. # Req: "No failing events happen in my drone" # Ex: For every event at every probe, if it has an outcome # value, verify that the outcome is never FAIL NEVER *@*(_.outcome = FAIL)
Example : An event is always followed by another event with a certain value within a time limit
- When you're checking events between probes with the same clock, you can constrain event relationships by time.
# Case: An event is always followed by another event # with a certain value, within a time limit. # Req: "Preflight checks always complete successfully # within the required amount of time (100 ms)." # Ex: For each time the event SENSORS_REQ_IN_PREFLIGHT_CHECKS # has a payload of true, verify that it is followed by an # expectation event PREFLIGHT_CHECK_COMPLETE with an # outcome of pass within 100 milliseconds. FOR EACH SENSORS_REQ_IN_PREFLIGHT_CHECKS@PX4_COMMANDER(_.payload = true) AS checkSensors VERIFY checkSensors -> WITHIN 100ms PREFLIGHT_CHECK_COMPLETE@PX4_COMMANDER(_.outcome = PASS)
Example: A labeled sequence of events is always followed by another event
- You can label a sequence of several events as the initial condition for behavior to verify.
# Case: A labeled sequence of events is always followed by another event. # Req: "Every time a roll is detected, the flight is terminated." # Ex: For each time event FAILURE_DETECTOR_UPDATE_STABLE occurs at probe # PX4_COMMANDER and is followed by event FAILURE_DETECTOR_STATUS_ROLL_ACTIVE # with a fail outcome, label that whole sequence as "rollAsserted". # Then, verify that rollAsserted is always followed # by the CRITICAL_FAILURE_DETECTED_TERMINATE event. FOR EACH FAILURE_DETECTOR_UPDATE_STABLE@PX4_COMMANDER -> FAILURE_DETECTOR_STATUS_ROLL_ACTIVE@PX4_COMMANDER(_.outcome=fail) AS rollAsserted VERIFY rollAsserted -> CRITICAL_FAILURE_DETECTED_TERMINATE@PX4_COMMANDER
Example: Many time-sensitive events happen in response to a condition
- You can always verify whether complex chains of events occurred in order.
- If multiple probes are instrumented with the same wall clock, you can verify that their events happen within time limits.
# Case: Many time-sensitive events happen in response to a condition # Req: "When there's an emergency stop command, the command # is processed quickly (50ms), and then landing # is successful within the required amount of time (10s)." # Ex: For each EMERGENCY_TERMINATION_REQUESTED event at PX4_COMMANDER probe, # label that event "emergencyTerminationRequested" and verify that # the event EMERGENCY_LANDING_INITIATED occurs within 50ms, followed by # the event LANDED at the PX4_LAND_DETECTOR probe within 10 seconds, # followed by the event LAND_DETECTED at PX4_COMMANDER within 50ms, # followed by a GROUND_TRUTH_ALTITUDE event with a payload of 0 # at the GAZEBO_SIMULATOR probe within 50ms. FOR EACH EMERGENCY_TERMINATION_REQUESTED@PX4_COMMANDER AS emergencyTerminationRequested VERIFY emergencyTerminationRequested -> WITHIN 50ms EMERGENCY_LANDING_INITIATED@PX4_COMMANDER -> WITHIN 10s LANDED@PX4_LAND_DETECTOR -> WITHIN 50ms LAND_DETECTED@PX4_COMMANDER -> WITHIN 50ms GROUND_TRUTH_ALTITUDE@GAZEBO_SIMULATOR(_.payload = 0)
# 5. Confirm the event names and probes names for your test query.
If you're modifying one of the example specification queries above, insert the appropriate names for the events and probes from your own system.
If you'd like to see the events available in your system, call
modality sut event list
$ modality sut event list NAME TAGS CONSUMER_REGISTERED [heartbeat, monitor] CONSUMER_TIMEOUT [heartbeat, monitor, timeout] DEINIT [consumer] DEINIT [producer] DEINIT [monitor] HEARTBEAT_ID_CHECK [heartbeat, monitor] ...
- If you'd like to see the probes available in your system, call
modality sut probe list
$ modality sut probe list NAME TAGS CONSUMER [c-example, consumer] MONITOR [c-example, monitor] PRODUCER [c-example, producer]
# 6. Save your completed system requirement query in your
<test-query-file.tq> text file.
This query file can be tested against any and every Modality-recorded session of your system.
In the next step, we'll record a session of your system in action.
# Step 2: Record Your Validation Session
Modality decouples the task of exercising your system from the task of checking your system. For this second step, you'll use Modality to record your system as it moves through the behaviors you want to verify.
# 1. Create a test-case-script to exercise your system. In this script:
Command your system to do whatever is relevant to your system requirement, whether that's an isolated task or a complex series of activities.
If your system requirement query is concerned with a certain period of system behavior, wrap Modality scopes around that portion.
- Scopes label regions of recorded system events that you can target with Modality queries afterwards.
modality session scope open <scope-name>at the start of each interesting period of system behavior.
modality session scope close <scope-name>at the end of each interesting period.
We recommend you wrap the whole test-case-script in a
<whole-test-case-scope>, for future use in a system validation test suite and elsewhere.
Modality scopes can be nested and overlap, so add as many or as few as you'd like.
In this first example test-case-script, a drone developer only wants to label the test case as a whole and a figure-eight maneuver:
modality session scope open drone-test-case-a drone-startup.sh drone-takeoff.sh modality session scope open figure-eight drone-figure-eight.sh modality session scope close figure-eight drone-landing.sh drone-shutdown.sh modality session scope close drone-test-case-a
In this second example test-case-script, a drone developer cares about the test case as a whole, plus start-up, flight, the midair figure-eight maneuver, and landing:
modality session scope open drone-test-case-b modality session scope open start-up drone-startup.sh modality session scope close start-up modality session scope open flight drone-takeoff.sh modality session scope open figure-eight drone-figure-eight.sh modality session scope close figure-eight modality session scope open landing drone-landing.sh modality session scope close landing modality session scope close flight drone-shutdown.sh modality session scope close drone-test-case-b
# 2. Record your validation session.
If you want to run your validation query as part of a larger test suite, skip to the Run A System Validation Test Suite section below.
If you want to record a single validation test case, write and then run a small test-lifecycle-script file to do the following:
Perform any system setup not included in your test-case-script, making your system ready for your test-case-script.
modality session open <validation-session-name> <system-under-test-name>to start a new recording session.
<validation-session-name>is the example session name we'll use below.
Run your test-case-script.
After the test-case script is complete, close the session by calling
modality session close <validation-session-name>
# Step 3: Test Your System Requirement
Now that your test case session has been recorded, all of your system's requirements can be tested at your leisure.
# 1. Call
modality session use <validation-session-name> to select the validation session you'd like to use as default.
- This can be the
<validation-session-name>you recorded in the previous step, or any other session of interest.
# 2. If you want to test your system requirement query over the entire recorded session, call
modality check --file <test-query-file.tq>
# Checks your test-query over your entire current default session $ modality check --file test-query-file.tq
# 3. If you want to test your system requirement query over a particular portion of recorded execution, call
modality check --file <test-query-file.tq> --region-expression <region-expression>
--region-expressionlets you define what regions your query will test, including sessions and scopes.
If you want to examine very specific periods, you can combine multiple conditions in your region expression.
For example, if you had a session called
validation-session-nameand a scope called
figure-eight, you could call
modality check --file test-query.tq --region-expression 'session="validation-session-name" AND scope="figure-eight"'to only test events that occurred within the figure-eight maneuver of that particular test session.
# Checks your test-query over just the figure-eight scope of events # inside the session-name session $ modality check --file test-query-file.tq --region-expression 'session="session-name" AND scope="figure-eight"'
modality check will return whether or not your system violated the terms of your system requirement query.
- In this example, we see that the
AFTER 600msconstraint is violated, and we also see that the session saw values up to
3182msbetween the selected events. Together, this gives us a hypothesis that some part of the system is creating a bottleneck.
$ modality check -v --file test-query-file.tq The given check had no matches. Analyzing why… Violation: Exists NEVER RECVD_MSG @ MONITOR(_.payload = 2) -> AFTER 600ms ^^^^^^^^^^^^^^ | Changing this limit to 3182ms causes this assertion to pass RECVD_MSG @ MONITOR(_.payload = 2)
# 5. If there is a check violation, your system isn't meeting the requirement specification.
The great news is that this process has equipped you and your team with strong leads to root out the cause with Modality.
Give your troubleshooting or development team the
<validation-session-name>used in your check. See How to Investigate the Cause of a Bug with Modality to make use of these tools for troubleshooting.
If you believe your test has found a possible edge case and you'd like to see what types of conditions it occurs in, see How to Reproduce a Bug with Modality.
If you would like additional details, you can call
modality check -vv --file <test-query-file.tq>for a counterexample and counter-query, then see How to Investigate the Cause of a Bug with Modality .
modality check -vv --file <test-query-file.tq>returns one sample counterexample, showing details from a test case where this measurement query failed.
- The returned
<counter-query>is an extremely helpful counterpart to your
<test-query>. While your requirement test query describes a property that should hold throughout your system, this corresponding
<counter-query>asks for all of the instances where that property is violated.
$ modality check -vv --file test-query-file.tq.tq The given check had no matches. Analyzing why… Violation: Exists NEVER RECVD_MSG @ MONITOR(_.payload = 2) -> AFTER 600ms ^^^^^^^^^^^^^^ | Changing this limit to 3182ms causes this assertion to pass RECVD_MSG @ MONITOR(_.payload = 2) Counter-Example: * RECVD_MSG@MONITOR(393359338:65560:23:6, RECVD_MSG@MONITOR, payload=2) ║ : (5 elided events) ║ * RECVD_MSG@MONITOR(393359338:131073:0:6, RECVD_MSG@MONITOR, payload=2) Counter-Query: RECVD_MSG @ MONITOR(_.payload = 2) -> AFTER 600ms RECVD_MSG @ MONITOR(_.payload = 2)
# 6. If there is no check violation but observed system behavior is still off-specification:
The test query as written may not be accurately describing the relevant system requirement behavior.
modality sut event listto see all of the events in your system, and consider instrumenting additional events on components that are related to this requirement.
Your test scripts may not be exercising enough of your system to capture the relevant system requirement behavior.
modality metrics coverage <region-expression>using the same
modality checkto see how much of your system is being exercised.
# 7. If there is no check violation, you can be confident that your system is performing according to your system requirement!
This system requirement test query can now be reused throughout the development process.
Consider adding this test query to your development team's integration or regression tests.
Your system requirement test query can also be added to your CI workflow.
For test engineers, we recommend adding this system requirement query to a system requirement validation test suite, so you can test all of your system requirements at once!
# Bonus: Run A Validation Test Suite
By adding each new system requirement query into a combined test suite, you can build a complete system requirement specification in Modality that can be tested with a single command.
One advantage of recording all of your test-suite-scripts together is that you may have previously scripted system behavior that you would now like to test with a newer system requirement query.
Fundamentally, this is a script to record and run all of your test-suite-scripts, and then call all of your test-query-files. Here's a simple example:
- Perform system setup
- Start a new recording session
modality session open <test-suite-session-name> <system-under-test-name>
- Run every test-case-script file
- Close the recording session
modality session close <test-suite-session-name>
- Check each of the test query files
modality check -v --file <test-query-file.tq> --region-expression <region-expression>"'
- For example, if you want to run a test query for a particular scope across all of the test cases:
$ modality check -v --file test-query-file.tq --region-expression 'session = "test-suite-session-name" AND scope = "particular-scope"'
- Pipe the output to the file or tool of your choice, and then see interpreting your results above.