Verified Component-based Software in SPARK: 
Experimental Results for a Missile Guidance System

Kung-Kiu Lau and Zheng Wang
School of Computer Science, The University of Manchester
Oxford Road, Manchester M13 9PL, United Kingdom
{kung-kiu,zw@cs.man.ac.uk}

Abstract:

SPARK is useful for developing reliable software for safety-critical 
systems, using the `correctness-by-construction' approach. It also has 
verification tools that can be used to produce verified software. 
To tackle larger-scale development of verified software, components 
are useful. In this paper we show how to define and implement software 
components in SPARK and use existing SPARK tools to produce verified 
component-based software. We demonstrate our approach on a missile 
guidance system.