Author: John W. McCormick, Peter C. Chapin
Pub Date: 2015
Size: 23 Mb
Software is pervasive in our lives. We are accustomed to dealing with the failures of much of that software – restarting an application is a very familiar solution. Such solutions are unacceptable when the software controls our cars, airplanes and medical devices or manages our private information. These applications must run without error. SPARK provides a means, based on mathematical proof, to guarantee that a program has no errors. SPARK is a formally defined programming language and a set of verification tools specifically designed to support the development of software used in high integrity applications. Using SPARK, developers can formally verify properties of their code such as information flow, freedom from runtime errors, functional correctness, security properties and safety properties. Written by two SPARK experts, this is the first introduction to the just-released 2014 version. It will help students and developers alike master the basic concepts for building systems with SPARK.
- High integrity applications are those whose failure has a high impact on humans, organizations, or the environment. Software quality is extremely important in such applications.
- Software quality should matter in all applications.
- The conformance of software to specifications and standards is an important, but not the only, aspect of software quality.
- A software defect is a difference between the behavior of the software and its specification.
- A correct program has no defects.
- The better the process used to develop software, the lower the defect rate.
- Testing alone is not adequate for developing high integrity software.
- Formal methods provide a means for producing software with fewer defects than that verified with testing.
- SPARK is a programming language specifically designed to support the development of software used in high integrity applications. It is an unambiguous subset of the Ada programming language.
- Static analysis is the examination of software without executing it. Static verification can only be done on programs written in unambiguous languages such as SPARK.
- The information provided by a static verification of a SPARK program can range from the detection of simple coding errors to a proof that the program is correct.
- GNATprove is the tool used to carry out the static verification of a SPARK program.
- An Ada compiler is used to translate a SPARK program into machine language instructions.
- Aspects are used to specify properties of entities.
Software Engineering with SPARK
In the preceding chapters we have concentrated on the details of the SPARK language. In this chapter, we look at a broader picture of how SPARK might be used in the context of a software engineering process. The SPARK 2014 Toolset User’s Guide (SPARK Team, 2014b) lists three common usage scenarios:
- Conversion of existing software developed in SPARK 2005 to SPARK 2014
- Analysis and/or conversion of legacy Ada software
- Development of new SPARK 2014 code from scratch
We start by examining each of these scenarios in more detail, discussing the interplay between proof and testing, and then presenting a case study to illustrate some issues arising when developing new SPARK 2014 code from scratch.
Creating New Software
SPARK is best applied to the development of new software. Starting from scratch provides the opportunity to make use of the SPARK tools from the development of the architectural design through the detailed implementation.
Test Driven Development (TDD) is a popular, evolutionary approach to software development that combines test-first development (in which you write a test before you write just enough code to fulfill that test) and refactoring (a disciplined restructuring of code). With SPARK’s ability to combine proof with testing, we can extend TDD to an even more rigorous approach we call Verification Driven Development (VDD). With VDD, we write contracts before we write the code to fulfill them. Data dependency and flow dependency contracts can be verified early on. Verification of freedom from runtime errors and of pre- and postconditions can be done once the code is written. Designing to meet your verification goals is a powerful approach to creating quality software.
Software design is all about the decisions a software engineer makes between the gathering and verification of requirements and the creation of code to implement those requirements. A design is the specification of a group of software artifacts or modules.
- The conversion of a SPARK 2005 program to SPARK 2014 is straight forward as SPARK 2014 is a superset of SPARK 2005.
- The SPARK tools may be used to perform retrospective analyses of existing Ada code where no SPARK aspects are given.
- The SPARK tools will generate safe over-approximations of data dependency contracts and flow dependency contracts directly from the source code of a program unit.
- More in-depth analyses of legacy Ada code may require moving non-SPARK code segments into child or private child packages.
- Designing to meet your verification goals is a powerful approach to creating quality software. This approach to creating new SPARK programs is called verification driven development.
- Abstraction, encapsulation, information hiding, coupling, and cohesion provide measures of good software design.
- The INFORMED design method was developed especially for applying the strengths of SPARK during this crucial stage of software development.
- The elements of an INFORMED design include variable packages, type packages, utility packages, boundary variable packages, and boundary variable abstraction packages.
- We use Abstract_State aspects to make it known that a package encapsulates state without revealing the implementation details of that state.
- Localizing state and minimizing data flow are major tenets of the INFORMED design method.
- Combining proof and testing is a powerful mechanism for verifying code. As the verification chain is only as strong as its weakest link, our goal is to obtain verification at least as good as can be accomplished with testing alone, but at a lower cost.