SPARK 2014

Expanding the boundaries of safe and secure programming

about-illustration

SPARK is a software development technology specifically designed for engineering high-reliability applications.

It consists of a programming language, a verification toolset and a design method which, taken together, ensure that ultra-low defect software can be deployed in application domains where high-reliability must be assured, for example where safety and security are key requirements.

SPARK has an enviable industrial track record. Over the past 25 years it has been applied worldwide in a range of industrial applications such as civil and military avionics, railway signalling, cryptographic and cross-domain solutions. SPARK 2014 is the next generation of this leading software technology, offering the following key benefits:

Flexibility

SPARK 2014 offers the flexibility of configuring the language on a per-project basis - applying restrictions that allow the fine-tuning of the permitted language features as appropriate to coding standards or run-time environments.

SPARK 2014 code can easily be combined with full Ada code or with C, meaning that new systems can be built on and re-use legacy code bases.

Powerful Static Verification

The SPARK 2014 language supports a wide range of different types of static verification. At one end of the spectrum is basic data and control flow analysis ie. exhaustive detection of uninitialized variables and ineffective assignment. For more critical applications, dependency contracts can be used to constrain the information flow allowed in an application. Violations of these contracts - potentially representing violations of safety or security policies - can then be detected even before the code is compiled.

In addition, the language is designed to support mathematical proof and thus offers access to a range of verification objectives: proving the absence of run-time exceptions, proving safety or security properties, or proving that the software implementation meets a formal specification of the program's required behaviour.

Ease of Adoption

SPARK 2014 is an easy-to-adopt approach to increasing the reliability of your software. Software engineers will find the SPARK 2014 language contains the powerful programming language features with which they are familiar, making the language easy to learn.

SPARK 2014 converges its contract syntax for functional behaviour with that of Ada 2012. Programmers familiar with writing executable contracts for run-time assertion checking will find the same paradigm can be applied for writing contracts that can be verified statically (ie. pre-compilation and pre-test) using automated tools.

Reduced Cost of Unit Testing

The costs associated with the demanding levels of unit testing required for high-assurance software - particularly in the context of industry standards such as DO-178 - are a major contribution to high delivery costs for safety-critical software. SPARK 2014 presents an innovative solution to this problem by allowing automated proof to be used in combination with unit testing to demonstrate functional correctness at subprogram level. In the high proportion of cases where proofs can be discharged automatically the cost of writing unit tests is completely avoided.

What’s New in SPARK 2014?

Convergence with Ada2012 Syntax

The latest version of the Ada language now contains contract-based programming constructs as part of the core language: preconditions, postconditions, type invariants and subtype predicates. SPARK 2014 uses the same syntax for contracts, meaning that a program written in Ada 2012 can be verified by the SPARK 2014 verification tools without having to rewrite the contracts. Subprograms in SPARK and in full Ada can now coexist more easily.

Using the Ada 2012 aspect notation, SPARK 2014 strengthens the specification capabilities of the language by the addition of contracts for:

  • Data dependencies
  • Information flows
  • State abstraction
  • Data and behaviour refinement

Selectable Language Profiles

Previous versions of SPARK embodied a set of restrictions essentially targeted at highly constrained run-time environments. SPARK 2014 provides the user with flexibility to choose their own language profile to suit their application environment: stay with the full language for server-based applications or apply the Strict profile for embedded applications with limited memory or minimal run-time support. Alternatively you can tailor the pre-defined profiles to prohibit particular language features according to project-specific constraints and regulations.

Hybrid Verification

Hybrid Verification is an innovative approach to demonstrating the functional correctness of a program using a combination of automated proof and unit testing. Once the functional behaviour or low-level requirements of a program have been captured as SPARK 2014 contracts, the verification toolset can be applied to automatically prove that the implementation is correct and free from run-time exceptions. Only where verification cannot be completed automatically is it necessary to write unit tests - with the same contracts used to check the correct run-time behaviour of the relevant subprograms.

Bigger Language Subset

The SPARK 2014 language comprises a much bigger subset of Ada than its predecessors. The only features excluded are those which are not amenable to sound static verification, which principally means access types, function side effects, aliasing, goto's, controlled types and exception handling.

Relative to previous versions of the language, the main additions to SPARK 2014 include:

  • Generic subprograms and packages
  • Discriminated types
  • Types with dynamic bounds
  • Array slicing
  • Array concatenation
  • Recursion
  • Early exit and return statements
  • Computed constants
  • A limited form of raise statements

Executable Contracts

Functional contracts (pre- and postconditions) have a dual purpose in SPARK 2014. As in previous versions of SPARK, they can be used to specify the functional behaviour required from a subprogram, against which its implementation can be statically verified (ie. pre-compilation) by the proof system that forms part of the toolset. In SPARK 2014, the same contracts can also be compiled and executed, which in practice means that the compiler turns them into run-time assertions. The executable semantics have a number of applications, not only hybrid verification, but also as an aid to the validation and development of the contracts themselves.

Generative Mode for Data Dependencies

When the implementation of a unit is available, the SPARK tools can extract the information flow and data dependencies for those subprograms in the unit. The user has the choice to specify information flow contracts on the code where they must be enforced, but otherwise let the tools generate the missing contracts to allow overall analysis to be completed.

Formal Container Library

SPARK 2014 excludes data structures based on pointers, because they make formal verification intractable. Instead, users can either hide pointers from client units by making the data structures private, or benefit from the library of formal containers provided with SPARK 2014. These generic containers (vectors, lists, maps, sets) have been specifically designed to facilitate the proof of client units.

 

Resources