This talk will consider a range of large, real-world projects that are using SPARK - an annotated sublanguage of Ada that is appropriate for the development of high-integrity systems.
Three projects will be considered in some detail where SPARK has made a contribution to meeting the most stringent software engineering standards. The projects are the Lockheed C130J Mission Computer (DO-178B Level A), the Ship/Helicopter Operational Limits Instrumentation System (UK Def. Stan. 00-55) and the MULTOS CA (a high-security system developed to meet the requirements of ITSEC E6). A less successful project will also be considered.
The lessons learned from these projects show that SPARK offers a cost-effective approach for the construction of high-integrity software when it is deployed judiciously within a software development process.