SPARK Pro is an integrated static analysis toolsuite for verifying high-integrity software through formal methods. It supports the SPARK 2014 language and provides advanced verification tools that are tightly integrated into the GNAT Programming Studio (GPS) and GNATbench IDEs.
Using SPARK Pro, developers can formally define and automatically verify software architectural properties, and guarantee a wide range of software integrity properties such as freedom from run-time errors, enforcement of security policies, and functional correctness (compliance with a formally defined specification) . This automated verification is particularly well-suited to applications where software failure is unacceptable. SPARK Pro helps reduce delivery costs and timescales, and through the use of formal methods it prevents, detects and eliminates defects early in the software lifecycle with mathematics-based assurance. The SPARK language and tools have a proven track record in the most demanding safety-critical and high-security systems.
SPARK provides an integrated approach to the entire software design and verification lifecycle – bringing software specification, coding, testing, and unit verification by proof within a single integrated framework. Verification goals that would otherwise have to be achieved by diverse techniques such as manual review can be met by applying the SPARK toolsuite, and reports can be generated to satisfy any evidential requirements.
Getting it right the first time
The SPARK technology supports design methods that allow programmers to verify the correctness of the software as it is being written. Investing effort early in the lifecycle to establish a sound foundation reduces the effort required in the test and debug phase, and it dramatically lowers the risk and cost associated with post-delivery defects. Partial programs can be analyzed, meaning that the benefits of automatic verification can be obtained right from the start of the development phase.
Complying with industrial safety standards
SPARK Pro meets the requirements of all high-integrity software safety standards, including DO-178B/C (and the Formal Methods supplement DO-333), CENELEC 50128 , IEC 61508, and DEFSTAN 00-56. The SPARK Pro toolset generates evidence that can be used to build a constructive assurance case and demonstrate conformance to the appropriate standard.
Provably secure software
SPARK Pro produces secure software that meets the requirements of the highest assurance levels of international standards such as the Common Criteria. The language and tools prevent and detect many of the most commonly occurring software security weaknesses such as buffer overflows and uninitialized variables. SPARK has been assessed in a report from the U.S. National Institute for Standards and Technology (NIST) as being more secure than many other commonly used programming languages.
Raising integrity of existing code
In addition to supporting the construction of new high-integrity applications, SPARK Pro can be applied to improve the quality of existing software. Ada code in the SPARK language subset can be analyzed for commonly-occurring errors such as uninitialized variables, or contracts can be incrementally added to support other modes of verification.