 |
SPARK Publications
Where indicated, PDF downloads of these publications are available
for download here. Where PDF is not available, please contact
us for how to obtain hardcopies.
These publications are now organised by sections, as follows:
Background and Motivation
Concepts and Methods
Industrial Experience and
Case Studies
Hardware Applications
Technical Reference
Theoretical Foundations
Background and
Motivation
"Logic versus
Magic in Critical Systems" 
(PDF 315kb)
© Springer-Verlag
Peter Amey, Praxis,
Lecture
Notes in Computer Science 2043
D. Craeynest and A. Strohmeier (Eds.):
Reliable Software Technologies – Ada-Europe 2001
6th Ada-Europe International Conference, Leuven, Belgium,
May 14-18, 2001.
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. This paper is one of
the keynote presentations at this year's Ada-Europe conference.
"Dear
Sir, Yours Faithfully: an Everyday Story of Formality"
(PDF 120kb)
Peter Amey, Praxis High Integrity Systems,
Invited keynote address, in "Practical Elements of Safety",
Proceedings of the Twelfth Safety-critical Systems Symposium,
Birmingham, UK, February 2004. Copyright Spinger-Verlag 2004.
ISBN 1-85233-800-8.
Abstract
This paper seeks a perspective on the reality of formal methods
in industry today. What has worked; what has not; and what
might the future bring? We show that where formality has been
adopted it has largely been beneficial. We show that formality
takes many forms, not all of them obviously "Formal Methods".
Concepts and Methods
"High-Integrity
Ada in a UML and C World"
(PDF 876kb)
© Springer-Verlag
Peter Amey and Neil White, Praxis,
Lecture
Notes in Computer Science 3063
A. Llamosi, A. Strohmeier (Eds.):
Reliable Software Technologies – Ada-Europe 2004
9th Ada-Europe International Conference, La Palma de Mallorca,
June 2004, pp. 225-236.
Abstract
The dictates of fashion and the desire to use "hot"
technology not only affects software developers but also influences
potential customers. Where once a client was just content
to accept something that worked (actually, would be delighted
to have something that worked) now they are concerned about
the means by which it was constructed; not just in the sense
of was it well-enough constructed but in the more
malign sense of was fashionable technology used. This
paper shows how the customer's desire to use de facto standards
such as UML and their wish to use language such as C—perhaps
to support a small or unusual processor; to integrate with
other subsystems; for the perceived comfort of future portability;
or for other, non-technical reasons—can be aligned with
the professional engineer's need to use those tools and languages
which are truly appropriate for rigorous software development.
"Static
Verification and Extreme Programming"
(PDF 252kb) Peter Amey and Roderick Chapman. Proceedings of
the ACM SIGAda Conference, December 2003.
Abstract
At first glance, the worlds of high-integrity software engineering
and Extreme Programming (XP) seem to have little in common.
Somewhat surprisingly, we have found the reverse to be the
case – indeed it seems that many practices advocated
by the XP community are familiar to us from many years' of
experience in building safety – and security-critical
systems. This paper discusses our experiences in applying
some XP practices in critical projects. Secondly, we discuss
how static verification can augment XP, particularly in the
Pairwise Programming and Refactoring practices.
"On the Principled
Design of Object-Oriented Programming Languages for High-Integrity
Systems"
(PDF 225kb) Roderick Chapman, Janet Barnes, and Brian Dobbing.
Submitted as a position paper to the 2nd NASA/FAA Object Oriented
Technology in Aviation Workshop.
Abstract
This paper describes the key properties and design principles
that make a programming language suitable for the construction
of high-integrity systems, with particular emphasis on object-oriented
language features, such as inheritance and dynamic-dispatch.
The paper goes on to describe how these principles have been
applied in the design of SPARK, which was recently extended
to include a subset of Ada95's tagged types facility. The
central thesis of the paper is that the ability to statically
analyse the behaviour of software should be a strong guiding
principle in the selection of language features for high-integrity
systems development – features that defy static analysis
and complicate verification should be excluded.
"Industrial Strength
Exception Freedom"
(PDF 231kb)
Roderick Chapman and Peter Amey, Praxis.
Proceedings of ACM SigAda 2002.
Abstract
Ada is unique amongst modern high-level languages in the degree
to which it allows programming errors to be trapped at the
compilation stage. Using a tool like the SPARK Examiner amplifies
this effect and can provide a high degree of confidence that
a program is well formed before we try and verify that its
behaviour is correct. Despite this progress a less tractable
class of errors remain: run-time exceptions. For safety-related
systems a run-time error may be just as hazardous as any other
logical error. For secure systems guarding against the deliberate
generation of such errors, through buffer overflow attacks
for example, is vital. The paper explains how automated techniques
based on formal verification or proof techniques have now
matured and provide an industrial strength solution.
"Correctness
by Construction: Better Can Also Be Cheaper"
(PDF 312kb) Peter Amey, Praxis. CrossTalk
Magazine, March 2002.
Abstract
For safety and mission critical systems, verification and
validation activities frequently dominate development costs,
accounting for as much as 80 percent in some cases. There
is now compelling evidence that development methods that focus
on bug prevention rather than bug detection can both raise
quality and save time and money. A recent large avionics project
reported a four-fold productivity and 10-fold quality improvement
by adopting such methods. A key ingredient of correctness
by construction is the use of unambiguous programming languages
that allow rigorous analysis very early in the development
process.
"The INFORMED Design Method for SPARK" Peter Amey,
Praxis, 1999, 2001. This paper is
available upon request. Please contact
us for details.
"Closing the loop
– The Influence of Code Analysis on Design"
(PDF 214kb)
© Springer-Verlag
Peter Amey, Praxis,
Lecture
Notes in Computer Science 2361
J. Bliebergerand A. Strohmeier (Eds.):
Reliable Software Technologies – Ada-Europe 2002
7th Ada-Europe International Conference, Vienna, June 2002
Abstract
Static code analysis originally concerned the extraction
from source code of various properties of a program. Although
this kind of reverse engineering approach can uncover errors
that are hard to detect in other ways, it is not a very efficient
use of resources because of its retrospective nature and the
late error detection that results. The SPARK language and
its associated Examiner tool took a different approach which
emphasises error prevention ("correctness by construction")
rather than error detection. Recent work with SPARK has shown
that very early application of static analysis can have a
beneficial influence on software architectures and designs.
The paper describes the use of SPARK to
produce designs with demonstrably low coupling and high cohesion.
"SPARK and Abstract Interpretation – A White Paper"
(PDF 204kb)
Rod Chapman, Praxis, September 2001
Introduction
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.
"A Language for
Systems not just Software"
(PDF 271kb)
Peter Amey, Praxis, September 2001.
This paper was presented at the ACM SigAda 2001 conference,
in Minneapolis, USA.
"The SPARK Way to Correctness is via Abstraction"
John Barnes, presented at Sig-Ada 2000.
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.
"Combining Static Worst-Case Timing Analysis and Program
Proof"
Roderick Chapman, Alam Burns, Andy Wellings. Real-Time Systems
Journal, Volume 11, pp145-171, 1996.
Industrial Experience
and Case Studies
"Correctness
By Construction: Developing a Commercial Secure System"
(PDF 358kb)
Anthony Hall and Roderick Chapman, IEEE Software, Jan/Feb
2002, pp18-25
Important Note:
This material is presented to ensure timely dissemination
of scholarly and technical work. Copyright and all rights
therein are retained by authors or by other copyright holders.
All persons copying this information are expected to adhere
to the terms and constraints invoked by each author's copyright.
In most cases, these works may not be reposted without the
explicit permission of the copyright holder.
"SPARK –
a state-of-the-practice approach to the Common Criteria implementation
requirements"
(PDF 223kb)
Rod Chapman, Praxis. Presented at
the 2nd International Common Criteria Conference, Brighton,
UK, July 2001
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 High Integrity Systems
using SPARK to meet the requirements of ITSEC E6.
"Cost-Effective Approaches to Safetify Safety-Critical
Regulatory Requirements"
James Sutton, Lockheed Martin, Presented in workshop session
at SigAda 2000.
"Industrial Experience with SPARK"
(PDF 234kb)
Dr. Roderick Chapman, Praxis High Integrity Systems Limted. Presented
at ACM SigAda 2000 conference.
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.
"SPARK
and the C130J Hercules II"
(PDF – 287kb)"
Praxis
This white paper discusses the lessons learnt and the benefits
gained through the use of SPARK during the redevelopment of
the Hercules aircraft.
"Re-engineering
a Safety-Critical Application with SPARK95 and GNORT"
(PDF 67kb)
Roderick Chapman and Robert Dewar,
Lecture
Notes in Computer Science 1622
Reliable Software Technologies – Ada-Europe '99
(c) Springer-Verlag 1999.
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.
"Is
Proof More Cost Effective Than Testing?"
(PDF 677kb)
Steve King, Jonathan Hammond, Rod Chapman and Andy Pryor,
IEEE Transactions on Software Engineering, Volume 26 Number
8.
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.
"Breaking Through the V and V Bottleneck"
(PDF 255kb)
Martin Croxford and James Sutton. Presented at Ada Europe
1995,
Published by Springer-Verlag in "Lecture Notes in Computer
Science" Volume 1031, 1996.
This paper presents a method of software development aimed
at "correctness by construction", which greatly
attenuates problems and costs associated with the detection
of errors at a late phase of the lifecycle. The process described
here has been applied successfully to the development of avionic
software for the C-130J aircraft.
Hardware Applications
"High-Integrity
Interfacing to Programmable Logic with Ada"
(PDF 318kb)
© Springer-Verlag
Adrian J Hilton, Praxis and
Jon G Hall, Open University.
Lecture
Notes in Computer Science 3063
A. Llamosi, A. Strohmeier (Eds.):
Reliable Software Technologies – Ada-Europe 2004
9th Ada-Europe International Conference, La Palma de Mallorca,
Spain, June 2004, pp. 249-260.
Abstract
Programmable Logic Devices (PLDs) are now common components
of safety-critical systems, and are increasingly used for
safety-related or safety-critical functionality. Recent safety
standards demand similar rigour in PLD specification, design
and verification to that in critical software design. Existing
PLD development tools and techniques are inadequate for the
higher integrity levels. In this paper we examine the use
of Ada as a design language for PLDs. We analyse earlier work
on Ada-to-HDL compilation and identify where it could be improved.
We show how program fragments written in the SPARK Ada subset
can be efficiently and rigorously translated into PLD programs,
and how a SPARK Ada program can be effectively interfaced
to a PLD program. The techniques discussed are then applied
to a substantial case study and some preliminary conclusions
are drawn from the results.
Technical Reference
"SPARK95 — The SPADE
Ada 95 Kernel (Including RavenSPARK)"
(PDF 371kb) Praxis, 2003.
This report 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.
Note
This report is written in the style of the Ada 95 Language
Reference Manual, and assumes familiarity with the structure
and terminology of that document. For a more friendly introduction
to SPARK, try the SPARK Book.
"SPARK – The SPADE Ada Kernel"
Praxis, 2003.
This report defines SPARK, an annotated subset of the Ada
83 language. It describes the differences between SPARK and
Ada and also defines the SPARK syntax. Please contact
us if you'd like a hardcopy of this report.
"The SPARK Ravenscar
Profile"
(PDF 258kb)
Praxis, 2003.
This report acts as a idiom guide and rationale for the RavenSPARK
extensions to SPARK.
"RavenSPARK Design for the
Minepump Case Study"
(PDF 174kb)
Praxis, 2003.
This report contains a worked example of the design of a RavenSPARK
program.
"High
Integrity Ravenscar"
(PDF 53kb)
Peter Amey and Brian Dobbing, 2003. From Proceedings of Reliable
Software Technologies – Ada Europe 2003.
Lecture
Notes in Computer Science Volume 2655
(c) Springer-Verlag 2003.
Abstract
The Ravenscar Profile is an exciting development for the Ada
community since it provides, for the first time in the history
of our industry, support for deterministic, multi-tasking
programming as an integral part of a standardized language.
Despite its many advantages, the profile leaves several areas
where behaviour is implementation defined and can result in
run-time errors; this is unfortunate in a profile aimed clearly
at the critical systems market. The SPARK language is a well-established
sequential Ada subset that avoids ambiguity and allows all
language rule violations to be detected prior to execution.
The authors show how the principles of SPARK have been successfully
extended to encompass the Ravencar Profile thereby statically
eliminating the profile’s problematic areas. The result
should allow concurrent Ada programs to be constructed with
the same degree of rigour that is now possible using sequential
SPARK.
"The Formal Semantics of SPARK83"
Ian O'Neill et. al., Program Validation Limited 1994.
These semantics reflect the SPARK83 language as-was in 1994.
Since then, the language has developed in several significant
areas. In particular, these semantics do not reflect SPARK95.
These documents are in PostScript format.
Volume 1 – Static Semantics. Please contact
us if you'd like a hardcopy of this report.
Volume 2 – Dynamic Semantics. Please contact
us if you'd like a hardcopy of this report.
The SPARK semantics were a product of QinetiQ's Systems Assurance
Group's research programme funded by TG10 of MOD's CRP.
Theoretical Foundations
"Information-Flow and Data-Flow Analysis of while-Programs"
Jean-Francois Bergeretti and Bernard A. Carré,
University of Southhampton.
Published in ACM Transactions on Programming Languages and
Systems.
Vol 7, No. 1, January 1985.
This paper explores the use of data- and information-flow
analysis as an aid to program development and validation,
and uses the information-flow relations from while-programs
to demonstrate how these relations may be used in writing,
testing and updating programs and also how they usefully extend
the class of errors that may be discovered through static
analysis.
We do not have PDF of this document. The ACM electronic library
does have it if you have access to that database.
|
|
