Define and Verify AI Constituent Requirements for ACAS Xu Neural Networks

Since R2026a

This example uses:

This example shows how to define, implement, and verify requirements for the ACAS Xu family of neural networks. This example is step 7 in a series of examples that take you through formally verifying a set of neural networks that output steering advisories to aircraft to prevent them from colliding with other aircraft.

To run this example, open Verify and Deploy Airborne Collision Avoidance System (ACAS) Xu Neural Networks and navigate to Step7DefineAndVerifyAIConstituentRequirementsForACASXuNeuralNetworksExample.m. This project contains all of the steps for this workflow. You can run the scripts in order or run each one independently.

Author the requirements using Requirements Editor (Requirements Toolbox), link each requirement to its implementation, and verify the requirements by using MATLAB® Test™ to run a suite of unit tests.

Types of Requirements

Requirements are a collection of statements that describe the desired behavior and characteristics of a system. Requirements ensure system design integrity and are achievable, verifiable, unambiguous, and consistent with each other. Each stage of design should have appropriate requirements.

This end-to-end example has two types of requirements:

AI Constituent — A set of requirements for the neural networks that issue collision avoidance advisories. You can split these requirements into two subsets: requirements for the model architecture and requirements for the model performance.
AI System — A set of requirements for the system that integrates the neural networks.

This example shows how to define, implement, and verify AI constituent requirements. For AI system requirements, see Define and Verify AI System Requirements for ACAS Xu Neural Networks Integrated Into Simulink.

Define Requirements

This example includes a small set of realistic requirements as illustration. If a system needs to meet specific safety criteria, then it will likely have many more requirements.

A requirement describes behavior that a design must satisfy. Requirements typically take the form of natural language statements, formulas, tables, and graphics. In Requirements Toolbox™, you use the Requirements Editor (Requirements Toolbox) to author requirements and create requirement sets to contain them. By linking one requirement set to another, you can trace each high-level requirement to its implementation. As the system design evolves, you can use iterative requirements analysis to enhance requirement traceability and coverage. You can use a traceability diagram to visualize requirement traceability.

In this example, the ACAS Xu neural networks must meet these architectural requirements:

There shall be one neural network for each of the 45 combinations of discrete values for time until loss of vertical separation and previous steering advisory.
Each neural network shall take a 1-by-5 dlarray with data format "BC" as input.
Each neural network shall return a 1-by-5 dlarray with data format "BC" as output.

The networks must meet these performance requirements:

The neural networks shall satisfy the Verification of Neural Networks Competition (VNN-COMP) properties described in Verify VNN-COMP Benchmark for ACAS Xu Neural Networks.

For information on how to add and manage requirements, see Use Requirements to Develop and Verify MATLAB Functions (Requirements Toolbox). The requirements for the AI constituents are attached to this example as a supporting file. Inspect the requirements in the Requirements Editor. Opening the file may take several minutes.

slreq.open(fullfile(matlab.project.rootProject().RootFolder,"requirements","AIConstituent.slreqx"));

Requirements for the AI constituents in the Requirements Editor.

Track Requirements Implementation

Each requirement has two properties that you can track:

Implemented — Indicates whether the requirement has been incorporated into the system or software design and development.
Verified — Indicates whether the implementation of the requirement passes the test and meets the specified criteria.

For example, a performance requirement for a neural network is implemented if the network architecture is known to be capable of fulfilling that requirement. The requirement is considered verified once a test shows that the network actually does fulfill the requirement.

You can view the implementation status of requirements in the Requirements Editor. Requirements Toolbox checks each functional requirement in a requirement set to see if it has an implementation link. Links point from the source item to the destination item and allow you to navigate between requirements in the Requirements Editor and their linked items, such as lines of MATLAB code, Simulink® blocks, and MATLAB and Simulink tests.

Implement Architectural Requirements

The neural networks are set up inside the convertACASXuFromONNXAndSave function, which is attached to this example as a supporting function. Each architectural requirement can be linked to the part of the code that implements it.

The first architectural requirement states: There shall be one neural network for each of the 45 combinations of discrete values for time until loss of vertical separation and previous steering advisory.

This requirement is implemented by having a separate network for each of the 45 possible pairings of discrete variables. The discrete variables can be traced to the filenames of the corresponding networks.

This example contains an implementation link from this requirement to line 21 of the convertACASXuFromONNXAndSave function. To learn how to create implementation links, see the Link Requirements to MATLAB Code (Requirements Toolbox) example.

Implementation link for the first architectural requirement in the Requirements Editor.

The next requirement states: Each neural network shall take a 1-by-5 dlarray with data format "BC" as input.

The code implements this requirement by preparing a featureInputLayer, with the number of inputs specified as 5, as the input layer for each network.

This example contains an implementation link from this requirement to line 111 of the convertACASXuFromONNXAndSave function.

Implementation link for the second architectural requirement in the Requirements Editor.

The last architectural requirement states: Each neural network shall output a 1-by-5 dlarray with data format "BC".

The code implements this requirement by preparing a fullyConnectedLayer, with the number of inputs specified as 5, as the output layer for each network.

This example contains an implementation link from this requirement to line 105 of the convertACASXuFromONNXAndSave function.

Implementation link for the third architectural requirement in the Requirements Editor.

Implement Performance Requirements

The performance requirement states: The ACAS Xu neural networks shall satisfy the VNN-COMP properties $ϕ_{1}, . . ., ϕ_{10}$ as described in Verify VNN-COMP Benchmark for ACAS Xu Neural Networks.

Each property can be considered to be a single requirement for each network to which it applies, resulting in a total of 186 individual requirements. The code does not explicitly implement these requirements in the same way it does the architectural requirements. Instead, these properties are considered implemented by justification: the depth and size of the networks is sufficiently large to enable the networks to satisfy the requirements.

In the Requirements Editor, justify the exclusion of the performance requirements from the implementation status by linking each requirement to a justification. Right-click each requirement and select Justification > Link with new Justification for implementation.

Verify Requirements

To verify the requirements, create tests, link the tests to the requirements, then run the tests.

In MATLAB, create tests using the unit test framework. For more information, see Class-Based Unit Tests.

Write your class-based unit tests as Test methods within your test class definition file. For example, write a test to verify the requirement that each network should have five output arguments. This test takes as input the two parameters identifying an individual network, TimeUntilLossOfVerticalSeparation and PreviousAdvisory, and checks that each network has the correct number of outputs.

function testNumNetworkOutputs(testCase,TimeUntilLossOfVerticalSeparation,PreviousAdvisory)
    % For each network, verify the number of outputs of the network
    % is 5
    net = helpers.loadACASNetwork(PreviousAdvisory,TimeUntilLossOfVerticalSeparation);
    numOutputs = net.Layers(end).OutputSize;
    verifyEqual(testCase,testCase.NumNetworkOutputs,numOutputs);
end

You can find the tests for this example in the tests file, attached to this example as a supporting file.

The performance tests do not rerun the analysis from Verify VNN-COMP Benchmark for ACAS Xu Neural Networks. Instead, the tests load the results file vnnlibResults.mat that you generated in that example and analyze its contents. If you have not run the Verify VNN-COMP Benchmark for ACAS Xu Neural Networks example, then this example uses a prepared results file, which is attached to this example as a supporting file.

Open and run the tests using MATLAB Test Manager using the matlabTestManager function.

matlabTestManager

Run all tests in the project by clicking the Run Tests button .

Performance test results in MATLAB Test Manager.

The majority of tests pass, but some fail. This is expected, since some of the VNN-COMP properties are unproven or violated. For more information, see Verify VNN-COMP Benchmark for ACAS Xu Neural Networks.

In the Requirements Editor, select Refresh to view the updated verification status of the requirements.

Generate Test Report

In MATLAB Test Manager, you can generate a report summarizing the test results. Click the View Reports button, then select Generate Test Result Report.

The test result report shows which tests passed and which tests failed. The report also details the reasons for any test failure. For example, the test testVNNLIB_phi2_net1_2 failed. This test checks whether the network for previous advisory Clear-of-Conflict and time until loss of vertical separation 1 second satisfies property $ϕ_{2}$ : if the intruder is distant and significantly slower than the ownship, then Clear-of-Conflict must never be the least likely choice.

Test result report for a failed verification test.

The report includes the adversarial example input that caused the test to fail: X = [55950 0.1186 -1.413 1185 41.12]. To confirm that this input violates $ϕ_{2}$ , load the corresponding network and predict the advisory.

timeUntilLossOfVerticalSeparation = 2;
previousAdvisory = 1;
net = helpers.loadACASNetwork(previousAdvisory,timeUntilLossOfVerticalSeparation);
X = [55950 0.1186 -1.413 1185 41.12];
yPred = predict(net,X)

yPred = 1×5 single row vector

    -1.0180    -0.7554    -0.7284    -1.0127    -0.6766

Find the class label corresponding to the minimum network output.

[~,idxOutputMin] = min(yPred);
helpers.classNames(idxOutputMin)

ans = 
"Clear-of-Conflict"

The network predicts Clear-of-Conflict as the least likely choice, which violates $ϕ_{2}$ .