Abstract Details
10/14/2015 | 2:00 PM - 2:45 PM | Pacific II
Hybrid Verification in SPARK 2014: Combining Formal Methods with Testing
Software defects in critical systems can have life-threatening consequences, and thus the verification process must provide high confidence that the software meets its requirements and does not contain vulnerabilities that could compromise its mission. Testing has been the traditional method for demonstrating the achievement of this goal, but it is well known that testing is intrinsically incomplete. For higher levels of confidence, static analysis and in particular formal methods are needed, in order to prove absence of run-time errors or the satisfaction of formally specified requirements.
Formal methods, however, require constraining the programming language constructs to features that can be analyzed mathematically. Since a large system may have components at different assurance levels, the components at lower levels of criticality do not need to be constrained to a formally analyzable subset; traditional testing techniques would be sufficient. What is needed is a language and supporting tools that allow the programmer to use the full language for components that do not require formal methods, and a formally analyzable subset for the critical components; and further to use the formally analyzable subset with either run-time checks (for initial testing) or static checks (rejecting the program if the checks can fail) to ease the transition from dynamic to static verification. The SPARK 2014 language, a formally analyzable subset of Ada 2012, was designed to meet these goals.
SPARK 2014 is an Ada 2012 subset that excludes difficult-to-analyze features such as pointers and dynamic allocation and that ensures deterministic (implementation-independent) semantics. SPARK 2014 provides full support for contract-based programming (pre- and postconditions, type invariants) and also allows the programmer to specify a module's data and flow dependence contracts, all through Ada 2012 syntax. An Ada 2012 program can have some parts in full Ada and other parts in the SPARK 2014 subset (specially marked as such). SPARK components can be compiled by a standard Ada compiler and will have standard Ada run-time semantics, but are amenable to a more formal treatment than full Ada.
An Ada 2012 program can thus be verified with a "hybrid" technique that combines formal methods and testing. In one possible scenario, a SPARK 2014 analysis tool can be used on dynamically tested unit bodies that are in full Ada or in SPARK but without contracts, to compute their implicit data dependence contracts. This approach allows formal methods to be introduced for critical components during the maintenance or upgrade of an existing code base. Another use case is to introduce contracts early and then to perform dynamic testing on those units whose contracts cannot be proved by the analysis tool. SPARK 2014 can thus be used at various levels depending on the project context and issues such as the integrity level for the software and the verification objectives that need to be met.
This presentation will summarize SPARK 2014 and show how hybrid verification can be used in practice.
Presentation:
This presentation has not yet been uploaded.
Handouts:
No handouts have been uploaded.
Stephen Baird (Primary Presenter), AdaCore, baird@adacore.com;
Steve Baird is a senior software engineer at AdaCore, a member of the ISO/IEC JTC1/SC22/WG9 Ada Rapporteur Group (the Ada
language maintenance group), and a member of the SPARK language design group.
