code analysis

file

Visible to the public Semi-automated Test Case Generation for ACAS X Implementation Validation

We present FastPACE (Provable Assertion Checking Engine), a weakest precondition analysis tool, developed for semi-automated generation of tests cases for the Test Suite of the Airborne Collision Avoidance System Xa/Xo (ACAS X). The ACAS X Test Suite will be used as part of an assurance argument for the system, showing that an implementation matches the system specification.