Template-based construction of verified software

The use of formal verification to prove the correctness of software is increasingly being mandated by international standards for the development of safety critical systems. While formal development environments exist to assist in formal software development, formal verification is still an extremely difficult and time-consuming task, requiring expert skills not possessed by the typical software engineer. The authors propose a component-based development approach, where the aim is not so much to make savings in the cost of implementation, but instead to reduce the amount of verification that the software engineer needs to perform, as well as reducing the complexity of any remaining verification. This is achieved by providing reusable design templates that have been verified offline by an expert in mathematical logic and theorem proving. An important feature of the template language is the presence of higher-order parameters, which enable templates to be defined that are more widely applicable, thus giving better value for the one-off verification effort.