HOME

TheInfoList



OR:

SPARK is a formally defined computer
programming language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming l ...
based on the Ada programming language, intended for the development of high integrity software used in systems where predictable and highly reliable operation is essential. It facilitates the development of applications that demand safety, security, or business integrity. Originally, there were three versions of the SPARK language (SPARK83, SPARK95, SPARK2005) based on Ada 83, Ada 95 and Ada 2005 respectively. A fourth version of the SPARK language, SPARK 2014, based on Ada 2012, was released on April 30, 2014. SPARK 2014 is a complete re-design of the language and supporting verification tools. The SPARK language consists of a well-defined subset of the Ada language that uses
contracts A contract is a legally enforceable agreement between two or more parties that creates, defines, and governs mutual rights and obligations between them. A contract typically involves the transfer of goods, services, money, or a promise to ...
to describe the specification of components in a form that is suitable for both static and dynamic verification. In SPARK83/95/2005, the contracts are encoded in Ada comments and so are ignored by any standard Ada compiler, but are processed by the SPARK "Examiner" and its associated tools. SPARK 2014, in contrast, uses Ada 2012's built-in "aspect" syntax to express contracts, bringing them into the core of the language. The main tool for SPARK 2014 (GNATprove) is based on the GNAT/GCC infrastructure, and re-uses almost the entirety of the GNAT Ada 2012 front-end.


Technical overview

SPARK utilises the strengths of Ada while trying to eliminate all its potential ambiguities and insecure constructs. SPARK programs are by design meant to be unambiguous, and their behavior is required to be unaffected by the choice of Ada
compiler In computing, a compiler is a computer program that translates computer code written in one programming language (the ''source'' language) into another language (the ''target'' language). The name "compiler" is primarily used for programs that ...
. These goals are achieved partly by omitting some of Ada's more problematic features (such as unrestricted parallel tasking) and partly by introducing contracts which encode the application designer's intentions and requirements for certain components of a program. The combination of these approaches allows SPARK to meet its design objectives, which are: * logical
soundness In logic or, more precisely, deductive reasoning, an argument is sound if it is both valid in form and its premises are true. Soundness also has a related meaning in mathematical logic, wherein logical systems are sound if and only if every formul ...
* rigorous formal definition * simple semantics * security * expressive power *
verifiability Verify or verification may refer to: General * Verification and validation, in engineering or quality management systems, is the act of reviewing, inspecting or testing, in order to establish and document that a product, service or system meets ...
* bounded resource (space and time) requirements. * minimal runtime system requirements


Contract examples

Consider the Ada subprogram specification below: procedure Increment (X : in out Counter_Type); In pure Ada this might increment the variable X by one or one thousand; or it might set some global counter to X and return the original value of the counter in X; or it might do absolutely nothing with X at all. With SPARK 2014, contracts are added to the code to provide additional information regarding what a subprogram actually does. For example, we may alter the above specification to say: procedure Increment (X : in out Counter_Type) with Global => null, Depends => (X => X); This specifies that the Increment procedure does not use (neither update nor read) any global variable and that the only data item used in calculating the new value of X is X itself. Alternatively, the designer might specify: procedure Increment (X : in out Counter_Type) with Global => (In_Out => Count), Depends => (Count => (Count, X), X => null); This specifies that Increment will use the global variable Count in the same package as Increment, that the exported value of Count depends on the imported values of Count and X, and that the exported value of X does not depend on any variables at all and it will be derived from constant data only. If GNATprove is then run on the specification and corresponding body of a subprogram, it will analyse the body of the subprogram to build up a model of the information flow. This model is then compared against that which has been specified by the annotations and any discrepancies reported to the user. These specifications can be further extended by asserting various properties that either need to hold when a subprogram is called (''
precondition In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification. If a precondition is violated, the effect of th ...
s'') or that will hold once execution of the subprogram has completed ('' postconditions''). For example, we could say the following: procedure Increment (X : in out Counter_Type) with Global => null, Depends => (X => X), Pre => X < Counter_Type'Last, Post => X = X'Old + 1; This, now, specifies not only that X is derived from itself alone, but also that before Increment is called X must be strictly less than the last possible value of its type (to ensure that the result will never overflow) and that afterwards X will be equal to the initial value of X plus one.


Verification conditions

GNATprove can also generate a set of verification conditions or VCs. These conditions are used to establish whether certain properties hold for a given subprogram. At a minimum, the GNATprove will generate VCs to establish that all run-time errors cannot occur within a subprogram, such as: * array index out of range * type range violation * division by zero * numerical overflow. If a postcondition or any other assertion is added to a subprogram, GNATprove will also generate VCs that require the user to show that these properties hold for all possible paths through the subprogram. Under the hood, GNATprove uses the Why3 intermediate language and VC Generator, and the CVC4, Z3, and Alt-Ergo theorem provers to discharge VCs. Use of other provers (including interactive proof checkers) is also possible through other components of the Why3 toolset.


History

The first version of SPARK (based on Ada 83) was produced at the
University of Southampton , mottoeng = The Heights Yield to Endeavour , type = Public research university , established = 1862 – Hartley Institution1902 – Hartley University College1913 – Southampton University Coll ...
(with UK
Ministry of Defence {{unsourced, date=February 2021 A ministry of defence or defense (see spelling differences), also known as a department of defence or defense, is an often-used name for the part of a government responsible for matters of defence, found in state ...
sponsorship) by Bernard Carré and Trevor Jennings. The name ''SPARK'' was derived from ''SPADE Ada Kernel'', in reference to the ''SPADE'' subset of the
Pascal programming language Pascal is an imperative and procedural programming language, designed by Niklaus Wirth as a small, efficient language intended to encourage good programming practices using structured programming and data structuring. It is named in honour of t ...
. Subsequently the language was progressively extended and refined, first by Program Validation Limited and then by Praxis Critical Systems Limited. In 2004, Praxis Critical Systems Limited changed its name to Praxis High Integrity Systems Limited. In January 2010, the company became Altran Praxis. In early 2009, Praxis formed a partnership with AdaCore, and released "SPARK Pro" under the terms of the GPL. This was followed in June 2009 by the SPARK GPL Edition 2009, aimed at the
FOSS Fos or FOSS may refer to: Companies * Foss A/S, a Danish analytical instrument company *Foss Brewery, a former brewery in Oslo, Norway * Foss Maritime, a tugboat and shipping company Historic houses *Foss House (New Brighton, Minnesota), United ...
and academic communities. In June 2010, Altran-Praxis announced that the SPARK programming language would be used in the software of US Lunar project ''
CubeSat A CubeSat is a class of miniaturized satellite based around a form factor consisting of cubes. CubeSats have a mass of no more than per unit, and often use commercial off-the-shelf (COTS) components for their electronics and structure. CubeSat ...
'', expected to be completed in 2015. In January 2013, Altran-Praxis changed its name to Altran which in April 2021 became Capgemini Engineering (following Altran's merger with
Capgemini Capgemini SE is a multinational information technology (IT) services and consulting company, headquartered in Paris, France. History Capgemini was founded by Serge Kampf in 1967 as an enterprise management and data processing company. The com ...
). The first Pro release of SPARK 2014 was announced on April 30, 2014, and was quickly followed by the SPARK 2014 GPL edition, aimed at the
FLOSS Free and open-source software (FOSS) is a term used to refer to groups of software consisting of both free software and open-source software where anyone is freely licensed to use, copy, study, and change the software in any way, and the source ...
and academic communities.


Industrial applications


Safety-related systems

SPARK has been used in several high profile safety-critical systems, covering commercial aviation (
Rolls-Royce Trent The Rolls-Royce Trent is a family of high-bypass turbofans produced by Rolls-Royce. It continues the three spool architecture of the RB211 with a maximum thrust ranging from . Launched as the RB-211-524L in June 1988, the prototype firs ...
series jet engines, the ARINC ACAMS system, the Lockheed Martin C130J), military aviation (
EuroFighter Typhoon The Eurofighter Typhoon is a European multinational twin-engine, canard delta wing, multirole fighter. The Typhoon was designed originally as an air-superiority fighter and is manufactured by a consortium of Airbus, BAE Systems and Leonar ...
, Harrier GR9, AerMacchi M346), air-traffic management (UK
NATS iFACTS Nats or NATS may refer to: Politics * National Party (South Africa) and its supporters * New Zealand National Party and its supporters * Scottish National Party and its supporters Sports * Syracuse Nationals, an NBA team currently known as th ...
system), rail (numerous signalling applications), medical (the LifeFlow
ventricular assist device A ventricular assist device (VAD) is an electromechanical device for assisting cardiac circulation, which is used either to partially or to completely replace the function of a failing heart. The function of a VAD differs from that of an artific ...
), and space applications (the Vermont Technical College CubeSat project).


Security-related systems

SPARK has also been used in secure systems development. Users include
Rockwell Collins Rockwell Collins was a multinational corporation headquartered in Cedar Rapids, Iowa, providing avionics and information technology systems and services to government agencies and aircraft manufacturers. It was formed when the Collins Radio C ...
(Turnstile and SecureOne cross-domain solutions), the development of the original MULTOS CA, the NSA Tokeneer demonstrator, the secunet multi-level workstation, the Muen separation kernel and
Genode Genode is a free and open-source software operating system (OS) framework consisting of a microkernel abstraction layer and a set of user space components. The framework is notable as one of the few open-source operating systems not derived fr ...
block-device encrypter. In August 2010, Rod Chapman, principal engineer of Altran Praxis, implemented Skein, one of candidates for
SHA-3 SHA-3 (Secure Hash Algorithm 3) is the latest member of the Secure Hash Algorithm family of standards, released by NIST on August 5, 2015. Although part of the same series of standards, SHA-3 is internally different from the MD5-like stru ...
, in SPARK. In comparing the performance of the SPARK and C implementations and after careful optimization, he managed to have the SPARK version run only about 5 to 10% slower than C. Later improvement to the Ada middle-end in GCC (implemented by Eric Botcazou of AdaCore) closed the gap, with the SPARK code matching the C in performance exactly. NVIDIA have also adopted SPARK for the implementation of security-critical firmware. In 2020, Rod Chapman re-implemented the TweetNaCl cryptographic library in SPARK 2014. The SPARK version of the library has a complete auto-active proof of type-safety, memory-safety and some correctness properties, and retains constant-time algorithms throughout. The SPARK code is also significantly faster than TweetNaCl.


See also

*
Z notation The Z notation is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general. History In 1974, Jean-Raymond Abrial ...
*
Java Modeling Language The Java Modeling Language (JML) is a specification language for Java programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm. Specifications are written as Java annotation comments to the ...


References


Further reading

* * *


External links


SPARK 2014 community site

SPARK Pro website

SPARK Libre (GPL) Edition website

Altran

Correctness by Construction: A Manifesto for High-Integrity Software

UK's Safety-Critical Systems Club



Tokeneer Project Page

Muen Kernel Public Release

LifeFlow LVAD Project

VTU CubeSat Project
{{DEFAULTSORT:Spark (Programming Language) Ada (programming language) Ada programming language family Algol programming language family Concurrent programming languages Formal specification languages High Integrity Programming Language History of computing in the United Kingdom Procedural programming languages Programming languages created in the 20th century Science and technology in Hampshire Statically typed programming languages Systems programming languages University of Southampton