This paper explores a new approach to validating soft- ware implementations that have been produced from formally-verified algorithms. Although visual inspection gives some confidence that the implementations faithfully reflect the formal models, it does not provide complete assurance that the software is correct. The proposed approach, which is based on animation of formal specifications, compares the outputs computed by the software implementations on a given suite of input val- ues to the outputs computed by the formal models on the same inputs, and determines if they are equal up to a given tolerance. The approach is illus- trated on a prototype air traffic management system that computes simple kinematic trajectories for aircraft. Proofs for the mathematical models of the system's algorithms are carried out in the Prototype Verification Sys- tem (PVS). The animation tool PVSio is used to evaluate the formal mod- els on a set of randomly generated test cases. Output values computed by PVSio are compared against output values computed by the actual soft- ware. This comparison improves the assurance that the translation from formal models to code is faithful and that, for example, floating point errors do not greatly affect correctness and safety properties.
['Aaron Dutle', 'César A. Muñoz', 'Anthony Narkawicz', 'Ricky W. Butler']
Software Validation via Model Animation