February 2016
32
T
ools
& S
oftware
Hybrid verification for
high-integrity software
By Benjamin M. Brosgol,
AdaCore
Testing has traditionally been
the principal way to verify that
software in a high-integrity system
meets requirements. Thanks to recent
advances in programming language
technology it is now practical to use
formal methods in conjunction with
testing, both lowering the cost of
verification and increasing the
confidence in the resulting product.
P
Q
P calls Q
P is
tested
Q is
proved
Q calls P
Figure 1. Combining tests and proofs
Verifica(on combining tests and proofs should be
at least as good as
verifica(on based on tests only
Suppose that a defect in your software can
lead to a catastrophic system failure, with a
resulting loss of life or other unacceptable con-
sequences. How do you achieve confidence
that the risk of such defects is eliminated, or
at least reduced to a tolerably low level? That
question has been on the minds of software
developers, regulatory agencies, and other
stake-holders since the earliest deployment
of computer-based systems in high-integ-
rity (e.g. safety-critical and/or high-security)
systems. Software defects (often euphemis-
tically referred to as glitches) can arise in
various ways, for example by installing the
wrong version of some component during an
update. This article focuses on the correctness
of the code itself: how to verify that the soft-
ware meets its requirements and has no unin-
tended behaviour.
Testing has traditionally been the main tech-
nique for software verification. However, the
observation of the late computer scientist Eds-
ger Dijkstra in 1969 still holds today: “Pro-
gram testing can be used to show the presence
of bugs, but never to show their absence.” Ide-
ally, we would like to be able to demonstrate,
with mathematical rigor, that our program
is correct. This is hardly a new idea; formal
methods (proofs of program properties such
as correctness) have been a subject of active
research since the 1960s. But for various rea-
sons this approach has been slow to make it
into the mainstream. Among the problems
is the need to restrict the programming lan-
guage to a subset that is formally analyzable,
and such subsets have typically been too con-
strained to be useful in practice. As another
issue, proof technology requires considerable
computing power and has not scaled up well
for realistic programs. There is also a percep-
tion that applying formal methods requires
a background in mathematical logic that is
outside the expertise of the domain special-
ists who develop the software. Finally and sig-
nificantly, there is a perceived methodological
issue; formal methods have a reputation for
requiring a particular development approach
that could not be easily introduced into a proj-
ect in an incremental fashion or combined
with traditional verification activities (in
particular, testing).
These issues, though challenging, are solvable;
this article will use the SPARK 2014 language/
verification technology as an illustration, with
a focus on how to combine formal methods
with testing. The goal of such hybrid verifica-
tion is to achieve a level of confidence at least
as high as would be obtained through testing
alone (figure 1). See the sidebar for a sum-
mary of SPARK 2014 (simply referred to as
SPARK below), which is a subset of the most
recent Ada language standard, Ada 2012.
Formal analysis is based on the concept of a
contract; an example of a subprogram with
precondition and postcondition contracts is
shown in figure 2 and is legal in both SPARK
and Ada. The precondition is a requirement
on the caller of the function, and it can be
assumed to be true in the body of the func-
tion. The postcondition is an obligation on the
implementation of the function, and it can be
assumed to be true by the caller after the func-
tion returns.
The Vector type is an array of integer values,
with different array objects possibly having
different lengths. The Min function requires
a non-empty Vector as its parameter, hence
its precondition states that the length must be
greater than zero. The postcondition expresses
the function guarantee: the result value is less
than or equal to each item in the Vector, and it
is one of the elements of the Vector.
The notion of a contract is not new; for exam-
ple it has been fundamental to the Eiffel lan-
guage since the early 1980s. The innovation
of the SPARK/Ada approach is the flexibility
that it offers, since a contract can be treated
in any of three ways based on the policy
selected by the program: evaluated at runtime
according to standard Ada semantics, raising
an exception if false, proved statically by the
SPARK tools, or else reported as not provable,
Figure 1. Combining tests and
proofs
