Checking aircraft requirements with Z3

Background

Before an aircraft is built, engineers write down what it has to do and how safe it has to be. These statements are called requirements. They start with the aircraft as a whole. Then they are broken down into requirements for each system, like the brakes, and then for each part of that system.

ARP4754B, published by SAE International, is a guideline for this process. Its Appendix E walks through one full example, following a wheel brake system from aircraft-level requirements down to the brake controller. Because each level is written up in its own documents, the same requirement gets restated across safety analyses, specifications and assumption lists. Every restatement is a chance for the meaning to shift. A condition gets dropped, a unit changes from per flight to per hour, or “above” becomes “at or above.” Each version still reads fine on its own, so across hundreds of pages these shifts are easy to miss.

We built specguard to catch these shifts. It converts each requirement into a precise logical statement. After a manual review, a solver called Z3 compares the statements and finds the exact cases where two versions of a requirement disagree. We ran it on 176 requirements and assumptions from Appendix E. The rest of this article explains how specguard works and walks through one of the problems it found.

This matters because every safety rule set early on has to survive into the final specification, and specguard shows exactly where one didn’t.

Method

specguard works in three steps. First, it reads a section of the standard and converts each requirement into a logical statement, keeping the requirement’s ID and original text alongside it. Second, the statements go through manual review. Third, the reviewed statements go to Z3, a logic solver that either finds values that make every statement true at once or proves that no such values exist.

The main check compares an earlier rule with a later version of it (the same rule, rewritten in a different section). Z3 searches for any situation the later rule allows but the earlier rule forbids. If there isn’t one, the check passes. If there is, the check fails, and Z3 shows the exact situation where the two rules split. The check only goes one way. The later rule is allowed to be stricter than the earlier rule, but it can’t be less strict. For example, if the earlier rule says the brakes must respond within 2 seconds, the later rule can require 1 second but not 3.

Some rules are supposed to stay exactly the same, like a limit copied from one table to another. For these, the one-way check isn’t enough. A pass only shows the later rule is as strict as the earlier one or stricter. If it is stricter, the two rules are not the same. So specguard runs the check both ways, and the rules only match if both checks pass.

Here is a small example of that double check. Say the original rule is “speed must be below 100” and a later document restates it as “speed must be at most 100.” The restatement is supposed to mean the same thing as the original, so we check it both ways.

The first check fails. The restatement is looser than the original, and Z3 finds the exact speed where they split, which is 100. The second check passes, because any speed below 100 is also at most 100. Both checks have to pass for the two statements to mean the same thing, so the restatement changed the rule.

Worked Example: the brake control gap

Across the 176 requirements and assumptions, our analysis found five logical inconsistencies between documents. Here we go through one of them.

The wheel brake system has two control signals. We will call them N, which turns on the normal brake control, and A, which turns on the alternate brake control. Early in the design, the safety analysis (Table E13, p. 137) requires exactly one of the two to be on at any time. It does this with two rules. The first says that if N is on, A must be off. The second says that if N is off, A must be on.

Later, the final specification for the brake system (Table E19, p. 144) restates these requirements. It keeps the first rule but leaves out the second.

Going through every combination of the two signals shows where the documents differ.

The last row is the problem. When both signals are off, neither brake control is on. The safety analysis forbids this, but the final specification allows it. specguard caught this with the one-way check described above. It asked Z3 whether there is any situation where everything in the final specification is followed but the second rule from the safety analysis is broken. Z3 answered yes and returned N off and A off, which is the last row of the table. So the check fails, and that state is the counterexample. If the second rule is added back into the final specification, the check passes.

Conclusion

Requirements can change slightly when they are restated, and when each document reads fine on its own, those changes are hard to spot. In the brake example, one missing rule meant the final specification allowed both brake controls to be off. specguard found it by converting the requirements into logic and letting Z3 search for a case where the two documents disagree. We think pairing automatic conversion with a solver like Z3 is an interesting direction to work on.

Everything behind this article is in the specguard repository. It has the Appendix E requirements as logical statements next to their original text, the solver that runs the checks, and the instructions specguard uses to convert a standard. You can rerun the whole analysis from the repository root with the two commands below and see the result of every check. No API key is needed.

pip install z3-solver
python solve.py

The repository also explains how to run the same checks on your own requirements.

Reference. SAE International, ARP4754B, Guidelines for Development of Civil Aircraft and Systems, December 2023, Appendix E, “Development Assurance Contiguous Example.”