AUTOSAC: Automated generation of tests from Spark Ada Contracts

A significant portion of the resources spent in the development of secure software is invested in the design, maintenance, and execution of tests based on low-level requirements. The AUTOSAC research project, funded by the National Aerospace Technology Exploitation Programme (NATEP), intends to address this problem by using contracts, a feature of the SPARK language.

AUTOSAC will demonstrate an innovative tool chain that automates the generation of unit tests whilst maintaining their value as a functional check against requirements, with the aim of reducing the effort currently spent using manual testing processes. The SPARK contracts will function as the specification of the low-level requirements of the unit under test as well as the success criteria for the tests. The resulting tool chain will cover the entire process, from the analysis of the source code leading to the generation of tests through to the execution of tests and the evaluation of results.

The project is a collaboration between Altran, Rolls-Royce Controls and Data Services, MBDA, the University of Oxford, and Rapita Systems lasting from January 2016 through March 2017.