Presented as part of the 2019 HCSS conference.
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.
