SPARK Language

The primary design goal of the SPARK language is to provide the foundations for a sound, formal verification framework and static analysis toolset. The latest version of the language, SPARK 2014, is based on Ada 2012. It embodies a large subset of Ada 2012, whilst prohibiting those features which are not amenable to static verification and furthermore can be the source of software defects.

sparklanguage-banner

One of the key features of the SPARK language is the ability to be able to express contracts i.e. statements about the program’s behavior that must be implemented correctly by the developer – and can be checked by the verification toolset. SPARK 2014 expresses contracts using the aspect notation that forms part of Ada 2012, thus allowing the developer to express both requirements and implementation within the same language framework. Learn more about the SPARK 2014 language at spark-2014.com.

sparkpro-gps

GPS – the GNAT Programming Studio IDE

The GPS Integrated Development Environment serves as your fully-integrated portal to the SPARK Pro static verification toolset. Errors and warnings generated by the tools are displayed as navigable messages mapped back to the source code with path information that helps to provide an understanding of how the errors can occur. GPS provides customizable settings, browsing, syntax-directed editing, easy integration with third party tools such as Version Control Systems, source navigation, dependency graphs, and more. Learn More »

SPARK 2005 to SPARK 2014 Translator

For customers with an established SPARK code base (using SPARK 83/95/2005), a tool is provided to assist with the translation process. Once translated into SPARK 2014, the code can be extended to take advantage of new features in the new expanded language and advanced toolset.

 

SPARK Pro Toolset

The SPARK Pro toolset is fully integrated with the GPS IDE, so that errors and warnings can displayed within the same environment as the source code thereby providing a smoother workflow for the developer. Alternatively, the tools can be run in command-line mode to generate the reports required for certification evidence.

The SPARK Pro toolset can perform a range of verification functions that are unrivalled in terms of soundness, low false alarm rate, depth and efficiency. These functions can be applied independently or in combination, as appropriate to the assurance strategy for the software under development.

Data Flow Analysis

Detects common programming errors that can be the cause of insecurities or erroneous behaviour, including uninitialised variables and ineffective assignments. Advanced data flow analysis can be used to check that access to global variables conforms to contracts specified by a software architect, thereby ensuring that the software conforms to its architectural design.

Information Flow Analysis

For more critical applications, dependency contracts can be specified to constrain the information flow allowed in a program. Violations of these contracts - potentially representing violations of safety or security policies - can then be detected even before the code is compiled.

Absence of Run Time Exceptions

SPARK Pro can check that a program is free from run-time exceptions such as divide-by-zero, numeric overflow, buffer overflows or indexing an array out-of-bounds. The mathematical proof system on which SPARK Pro is based guarantees that this analysis is sound, so that even before a program is executed or tested or large class of potentially hard-to-detect errors can be eliminated from your software.

Property Checking

For more critical applications, key safety or security properties can be expressed in the contract notation that forms part of Ada 2012. Using a mathematically-sound proof system, the SPARK Pro toolset is able to automatically check that a program will satisfy these properties for all possible inputs and execution paths - as if the program had been exhaustively tested but without ever having to compile or run the code.

 

Functional Correctness

With its extended contract language, SPARK provides for fully comprehensive, formal specification of the required functional behaviour of a program ie. a specification of the Low-Level Requirements. Using the same proof system, the SPARK Pro tools will automatically prove that a program meets its functional specification, thus providing the highest possible level of assurance for the correct behaviour of critical systems.