SPARK95(ID:3512/spa011)

Provable Ada95 

SPARK subset for Ada95
Related languages
Ada 95 => SPARK95   Subset
SPARK => SPARK95   Evolution of
References:
  • "SPARK95 — The SPADE Ada 95 Kernel" Praxis Critical Systems Limited, 1999. view details Abstract: This paper defines SPARK 95, an annotated subset of the Ada 95 language. It describes the differences between SPARK 95 and Ada 95 and defines the SPARK 95 syntax.
  • Chapman, Roderick and Dewar, Robert "Re-engineering a safety-critical system with SPARK95 and GNORT" view details Abstract: A paper about porting the SHOLIS project software to SPARK95 using ACT's GNAT-No-Runtime (GNORT) technology. This paper was presented at the 1999 Ada Europe conference, and went on to win the conference prize for best presentation. pdf
          in Reliable Software Technologies - Ada-Europe '99 LNCS 1622 1999 view details
  • King, Steve; Hammond, Jonathan; Chapman,Rod and Andy Pryor "Is Proof More Cost Effective Than Testing?" view details Abstract: A paper, originally appearing in 1999 World Congress on Formal Methods, but re-published in IEEE Transactions on Software Engineering. Considers the use of Z, SPARK and Proof in the SHOLIS project and compares the effectiveness of proof with other, more traditional verification activities. pdf
          in IEEE Transactions on Software Engineering 26(8) view details
  • "The SPARK Way to Correctness is via Abstraction" John Barnes, Presented at Sig-Ada 2000. view details Abstract: Abstraction is a key concept in the design and implementation of systems. In a good system, the various components will interact only through well-defined interfaces — in Ada, these interfaces are provided through package specifications. However, subprogram specifications do not limit the behaviour of the subprogram, they only define how the subprogram is called. The use of SPARK allows Ada specifications to be strengthened to several levels — at the simplest level, SPARK annotations will prevent unexpected side-effects, while at the highest level, SPARK can lead to complete proofs of correctness.
          in IEEE Transactions on Software Engineering 26(8) view details
  • Dr. Roderick Chapman "Industrial Experience with SPARK" Praxis Critical Systems Limted, Presented at ACM SigAda 2000 conference view details Abstract: This paper discusses three large, real-world projects (C130J, SHOLIS and the MULTOS CA) where SPARK has made a contribution to meeting stringent software engineering standards. pdf
          in IEEE Transactions on Software Engineering 26(8) view details
  • "SPARK and Abstract Interpretation—A White Paper" Rod Chapman, Praxis Critical Systems Limited, September 2001 view details Abstract: Recently, there has been significant interest in the use of Abstract Interpretation (AI) technology in the static analysis of critical software. A number of AI-based tools exist, but some of their marketing suffers from a level of hyperbole that is at best optimistic, and at worst somewhat irresponsible.

    There have also been some attempts to compare AI-based static analysis tools with the analysis implemented by the SPARK language and the SPARK Examiner toolset. The aim of this white paper is to dispel some of the common myths and to avoid potential confusion with customers.
    pdf
          in IEEE Transactions on Software Engineering 26(8) view details
  • Amey, Peter "Logic versus Magic in Critical Systems" view details Abstract: This paper discusses the prevailing trends to hide or magic away the complexity of a solution and contrasts these trends against the need to be able to reason logically about the behaviour of a Safety Critical system. pdf
          in Reliable Software Technologies (D. Craeynest and A. Strohmeier (Eds.)) - Ada-Europe 2001 Proceedings of 6th Ada-Europe International Conference, Leuven, Belgium, May 14-18, 2001 LNCS 2043 Springer view details
  • Rod Chapman "SPARK - a state-of-the-practice approach to the Common Criteria implementation requirements" presented at the 2nd International Common Criteria Conference, Brighton, UK, July 2001 view details Abstract: The Common Criteria (CC) require the use of programming languages whose statements have an "unambiguous meaning." This presentation considers SPARK: a widely-used language that is perhaps unique in actually meeting this requirement. While SPARK has its roots in security research, it is currently most widely used in the aerospace and rail industries, and has a well-established track record in meeting the most demanding standards in these domains, such as UK Def. Stan. 00-55 (for military systems) and DO-178B (for civil aviation). SPARK has recently proven, though, to be ideally suited to the development of secure systems.

    The design principles of SPARK will be described, highlighting the language's suitability for meeting the requirements of secure systems development. SPARK's static analysis tool (the Examiner) will also be considered, concentrating on the types of analysis, such as information flow analysis and proof of exception freedom, that can be achieved. The strengths of the language will be illustrated with reference to the MULTOS Global Key Centre (MGKC) - the system at the heart of the MULTOS CA - which was developed by Praxis Critical Systems using SPARK to meet the requirements of ITSEC E6.
    pdf
          in Reliable Software Technologies (D. Craeynest and A. Strohmeier (Eds.)) - Ada-Europe 2001 Proceedings of 6th Ada-Europe International Conference, Leuven, Belgium, May 14-18, 2001 LNCS 2043 Springer view details