Brief Information on Spark  
STAD, OU - Prof. J. Laski & P. Luczycki
 
Procomp, OU - Prof. J. Laski & W. Szermer & W.F. Stanley
 
Swat, Softools Inc.,
 
Short Introduction to VDM-Tools
 
back to main page

     
Short Introduction to Spark Systems   

Spark

Spark  is a high level Ada 95-based programming language
designed for the development of software of High Integrity or Safety Critical
applications, i.e. ones where life or the environment are at risk if the program
is in error.

Essentially, SPARK is an Ada 95 design language. It accepts a "Safety Critical" kernel
of Ada 95 e.g. by not allowing GOTOs or access variables pointers.  It also
introduces annotations  which are used to specify
the semantics of SPARK subprograms (procedures, functions). The annotations
describe the intended properties of a subprogram, e.g. its specification,
expected properties of the code (assertions) or input-output functionality.

As the annotations express the intended properties of the procedure, they are used
by SPARK to verify whether the code is consistent with them. There are three levels
of analysis carried out by SPARK, depending on the desired level of confidence in
the program.
  • Data Flow Analysis identifies some data flow anomalies in the program,
    e.g. the use of uninitializaed variables; no annotations are needed for that
    kind of analysis.
  • Information Flow Analysis checks the code against
    the user-defined annotations.
  • Formal Proofcan be carried out for the most critical
    subprorams.
SPARK is essentialy a design system, since no executable code is generated. Thus,
an Ada compiler is needed to generate the code. However,the use of SPARK at the early
stages of program development increases the likelihood of the program behaving
as intended and thereby significantly reduces the amount of testing.

Examples of proof annotations:
      derive annotations, i.e. the intended dependencies between
        OUT and IN variables
      pre- and post-conditions of subprograms
      assertions, e.g.  loop invariants
      declarations of proof functions.

Tool Support :

      Spark Examiner
      Spade Simplifier
      Spade Proof Checker


Currently, Spark is used in
  • CSE 438/538   Verification of Computer Programs.

    It is also planned to use Spade Proof Checker in

  • CSE 510   Fundamentals of Software Engineering Modelling,
    to support the deductive and transformational proofs.

For more information click on one of the below:


Praxis Critical Systems


For Instructions on how to Install and Run - Spark - Click here.