|
SPARK is a secure, formally-defined language designed to support the development of software used in applications where correct operation is vital either for reasons of safety or business integrity. There are versions of SPARK based on Ada 83 and Ada 95. The latest revision of the language, RavenSPARK, includes the Ravenscar Tasking Profile to support concurrency in high integrity applications. The formal, unambiguous definition of SPARK allows and encourages a variety of static analysis techniques to be applied to SPARK code. Software maintenance is one of the activities in software engineering, and is the process of enhancing and optimizing deployed software (software release), as well as remedying defects. ...
A software release is to create a new version of the system or program and release it to the user community. ...
In computing, an operating system (OS) is the system software responsible for the direct control and management of hardware and basic system operations. ...
Tux, a penguin, is the official Linux mascot. ...
Microsoft Windows is a range of commercial operating environments for personal computers. ...
OpenVMS (Open Virtual Memory System or just VMS) is the name of a high-end computer server operating system that runs on the VAX and Alpha family of computers developed by Digital Equipment Corporation of Maynard, Massachusetts (now owned by Hewlett-Packard); it has also recently been ported to servers...
Jump to: navigation, search The Solaris Operating System is a computer operating system, based on the open-source UNIX SunOS developed by Sun Microsystems. ...
A software genre is a classification of software by its common function, type or topic. ...
A programming language or computer language is a standardized communication technique for expressing instructions to a computer. ...
A software license is a type of proprietary or gratuitous license as well as a memorandum of contract between a producer and a user of computer software — sometimes called an End User License Agreement (EULA) — that specifies the perimeters of the permission granted by the owner to the user. ...
The front page of the English Wikipedia website. ...
Ada is a structured, statically typed imperative computer programming language designed by a team lead by Jean Ichbiah of CII Honeywell Bull during 1977–1983. ...
The Ravenscar profile is a subset of the Ada tasking features. ...
Technical Overview SPARK exploits the strengths of Ada while eliminating all its potential ambiguities and insecurities. A SPARK program has a precise meaning which is unaffected by the choice of Ada compiler and can never be erroneous. These desirable goals are achieved partly by omitting some of Ada's more problematic features (such as unrestricted tasking) and partly by introducing annotations or "formal comments" to capture the code designer's intentions.
The combination of these approaches allows SPARK to meet its design objectives which are:
- rigorous definition
- simple semantics
- security
- expressive power
- verifiability
- bounded resource requirements.
As SPARK is an annotated subset of Ada, programs written in SPARK can be compiled by any Ada compiler.
Tool Support The SPARK Examiner (part of the SPARK Toolset available from Praxis High Integrity Systems Ltd) performs two kinds of static analysis. The first, made up of language conformance checks and flow analysis, checks that the program is "well-formed" and is consistent with the design information included in its annotations. This stage is extremely straightforward and can be readily incorporated into the coding phase of the development process. After these checks the source is known to be free from erroneous behaviour and free from conditional and unconditional data flow errors (i.e. use of uninitialised data) on a system-wide basis (including abstract state in package bodies).
The second, optional, kind of analysis is verification: showing by proof that the SPARK program has certain specified properties. The most straightforward is a proof that the code is exception free; this adds Constraint_Error to the list of possible errors eliminated by SPARK. Proof can also be used to demonstrate, unequivocally, that the code maintains important safety or security properties or even to show its complete conformance with some suitable specification.
Full information on the static analysis techniques that may be performed using the SPARK Toolset is available at http://www.praxis-his.com/sparkada/examiner.asp
Annotation Examples Consider the Ada subprogram specification below: procedure Increment (X : in out Counter_Type); What does this subprogram actually do? In pure Ada, it could do virtually anything - it might increment the 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, annotations 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); --# derives X from X; or procedure Increment (X : in out Counter_Type); --# global Count; --# derives --# Count from Count, X & --# X from ; This first of these specifications tells us that the Increment procedure does not update or read from any global variables and that the only data item used in calculating the new value of X is X itself. The second set of annotations tells us that Increment will use some global variable called "Count" in the same package as Increment and that the exported value of Count is dependant on the imported values of Count and X, but that exported value of X does not depend on any variables at all -- it will be derived simply from constant data.
If the Examiner 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.
We can further extend these specifications by asserting various properties that either need to hold when a subprogram is called (preconditions) 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); --# derives X from X; --# pre X < Counter_Type'Last; --# post X = X~ + 1; This specification now says that not only is X only derived from itself, but that before Increment is called X must be strictly less than the last possible value of its type and that afterwards X will be equal to the initial value of X plus one -- no more and no less.
Verification Conditions The Examiner can be requested to generate a set of Verification Conditions or VCs. VCs are used to attempt to establish certain properties hold for a given subprogram. At a minimum, the Examiner will generate VCs attempting to establish that the following run-time errors cannot occur within a subprogram: - array index out of range
- type range violation
- division by zero
- numerical overflow
If a postcondition is added to the specification, the Examiner will also generate VCs that require the user to show that the postcondition will hold for all possible paths through the subprogram.
Discharging these proof obligations is performed using the SPADE Simplifier (an automated theorem prover) and the SPADE Proof Checker (a manual theorem prover, used for those VCs too thorny for the Simplifier to automatically discharge).
History of SPARK The first version of SPARK (based on Ada 83) was produced at the University of Southampton (with UK Ministry of Defence sponsorship) by Bernard Carré and Trevor Jennings. Subsequently the language was progressively extended and refined, first by Program Validation Limited and then by Praxis Critical Systems Ltd. In 2004, Praxis Critical Systems Ltd changed name to Praxis High Integrity Systems Ltd.
References John Gilbert Presslie Barnes is a British computer scientist. ...
John Gilbert Presslie Barnes is a British computer scientist. ...
IEEE Spectrum is a magazine edited by the Institute of Electrical and Electronics Engineers. ...
External links | 
Feeds |
Contact