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.
2008
"Use of Ada in Student CubeSat Project"
Carl Brandon, in "Reliable Software Technologies - Ada Europe 2008"
2007
"Using SMT Solvers to Verify High-Integrity Programs"
Paul B. Jackson, Bill J. Ellis and Kathleen Sharp.
2nd International Workshop on Automated Formal Methods, AFM '07, Atlanta, Georgia, USA, 6th November 2007.
2006
"Engineering the
Tokeneer Enclave Protection Software" 
/ 482kb PDF
Janet Barnes, Rod Chapman: Praxis High Integrity Systems.
Randy Johnson, James Widmaier: National Security Agency. David
Cooper: River River Limited. Bill Everett: SPRE Inc.
Proceedings of the IEEE International Symposium on Secure
Software Engineering (ISSSE) 2006.
Click here for an abstract...
The Tokeneer ID Station (TIS)
project, carried out by Praxis High Integrity Systems in conjunction
with SPRE Inc. under the direction of NSA, has shown that
it is possible to produce high quality, low defect systems
conforming to the Common Criteria requirements for Evaluation
Assurance Level 5 (EAL5). We state the seven guiding principles
we used to achieve this, and relate each one to examples from
the TIS development. The systems development industry in general
has viewed conformance with the Common Criteria higher levels
as too difficult, too expensive, and generally not economical.
The experience of Praxis High Integrity Systems, however,
is that the levels of EAL5 and beyond (including EAL7) are
achievable in a cost-effective manner. This TIS project was
commissioned as a demonstration vehicle, to show exactly how
the development approach adopted by Praxis matches up to EAL5,
and to measure its actual productivity and defect rates under
controlled conditions.
2005
"Modeling
SPARK systems with UML"
Xavier Sautejeau - Sodius
Proceedings of the ACM SIGAda Annual International Conference
(SIGAda 2005), November 2005
Click here for an abstract...
In this paper, we will consider two aspects of UML in order
to assess how well suited it is for modeling SPARK systems.
The first aspect is the ability to represent SPARK in UML
from a theoretical perspective. The second aspect is more
from a hands-on perspective and evaluates what makes a UML
CASE-tool more suitable for modeling SPARK systems than another.
"Optimizing
the SPARK program slicer"
Ricky E. Sward, Leemon C. Baird, Department of Computer Science,
US Air Force Academy, CO
Proceedings of the ACM SIGAda Annual International Conference
(SIGAda 2005), November 2005
Click here for an abstract...
Recent trends in software re-engineering have included tools
to extract program slices from existing Ada procedures. One
such tool has already been developed that extracts program
slices from SPARK procedures along with a proof that the functionality
of the original procedure is equivalent to the functionality
of the collection of resulting slices. This paper extends
this work by showing how assumptions in the proof can cause
inefficiencies in SPARKSlicer and by presenting alternatives
that optimize out the inefficiencies. The original proof is
modified to show that the SPARK program slicer still produces
functionally equivalent program slices from SPARK procedures
with these optimizations.
"Experiences
using SPARK in an Undergraduate CS Course"
Dr Anthony S Ruocco, Roger Williams University
Proceedings of the ACM SIGAda Annual International Conference
(SIGAda 2005), November 2005
Click here for an abstract...
This paper describes experiences garnered while teaching a
course on high integrity software using SPARK to a mix of
junior and senior level undergraduates. The paper describes
the impact of pre-requisites, course layout and execution,
and lessons learned by students and the instructor. The course
used the SPARK toolset provide by Praxis High Integrity Systems,
and the Gnat Programming System (GPS) provided by AdaCore
Technologies (ACT) under the Ada Academic Initiative Program.
Details about using these tools is integrated through out
the paper.
"The
Affordable Application of Formal Methods to Software Engineering"
James F Davis, University of Maryland University College
Proceedings of the ACM SIGAda Annual International Conference
(SIGAda 2005), November 2005
Click here for an abstract...
The purpose of this research paper is to examine (1) why formal
methods are required for software systems today; (2) the Praxis
High Integrity Systems' Correctness by Contruction methodolgy;
and (3) an affordable application of a formal methods methodology
to software engineering.
Languages,
Ambiguity, and Verification / SPARK team
Verified
Software: Theories, Tools, Experiments, ETH Zürich
10-13 October 2005
Click here for an abstract...
This position paper is based on presentations given at the
Grand Challenge workshops held at Gresham College in March
2004 and in Newcastle in July 2005. It reports some of our
experience from building the SPARK lan-guage and its verification
tools. We argue that the provision of an unambiguous semantics
for a programming language is crucial if the verification
framework is to be sound, deep and efficient. Secondly, we
offer some reflections on the (mostly non-technical) barriers
that we encounter in trying to deploy SPARK within organizations.
Finally, we try to set some goals for future.
Smart Certification Of Mixed Criticality Systems / 75kb PDF
Peter Amey, Rod Chapman, Neil White, Praxis High Integrity
Systems
AdaEurope 2005
Click here for an abstract...
High integrity applications, such as those performing safety
or security
critical functions, are usually built to conform to standards
such RTCA DO-
178B [1] or UK Def Stan 00-55 [2]. Typically such standards
define ascending
levels of criticality each of which requires a different and
increasingly onerous
level of verification. It is very common to find that real
systems contain code of
multiple criticality levels. For example, a critical control
system may generate
a non-critical usage log. Unless segregation can be demonstrated
to a very high
degree of confidence, there is usually no alternative to verifying
all the software
components to the standard required by the most critical element,
leading to an
increase in overall cost. This paper describes the novel use
of static analysis to
provide a robust segregation of differing criticality levels,
thus allowing appropriate verification techniques to be applied
at the subprogram level. We call this
fine-grained matching of verification level to subprogram
criticality smart certification.
2004
Enforcing Security and Safety Models with an Information
Flow Analysis Tool / 125kb PDF
Rod Chapman and Adrian Hilton, Praxis High Integrity Systems
SIGAda 2004.
"High-Integrity
Ada in a UML and C World" / 857kb PDF
(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.
Click here for an 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.
"High-Integrity
Interfacing to Programmable Logic with Ada" / 312kb PDF
© 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.
Click here for an 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.
"An Integration of Program Analysis and Automated Theorem Proving"
Bill J. Ellis and Andrew Ireland, Heriot-Watt University
Integrated Formal Methods: 4th International Conference, IFM
2004,
Click here for an abstract...
Finding tractable methods for program reasoning remains a
major research challenge. Here we address this challenge using
an integrated approach to tackle a niche program reasoning
application. The application is proving exception freedom,
i.e. proving that a program is free from run-time exceptions.
Exception freedom proofs are a significant task in the development
of high integrity software, such as safety and security critical
applications. The SPARK approach for the development of high
integrity software provides a significant degree of automation
in proving exception freedom. However, when the automation
fails, user interaction is required. We build upon the SPARK
approach to increase the amount of automation available. Our
approach involves the integration of two static analysis techniques.
We extend the proof planning paradigm with program analysis.
"Invariant
Patterns for Program Reasoning"
Andrew Ireland, Bill J. Ellis and Tommy Ingulfsen, Heriot-Watt
University
MICAI 2004: Advances in Artificial Intelligence: Third Mexican
International Conference on Artificial Intelligence
Click here for an abstract...
We address the problem of integrating standard techniques
for automatic invariant generation within the context of program
reasoning. We propose the use of invariant patterns which
enable us to associate common patterns of program code and
specifications with invariant schemas. This allows crucial
decisions relating to the development of invariants to be
delayed until a proof is attempted. Moreover, it allows patterns
within the program to be exploited in patching failed proof
attempts.
"Dear
Sir, Yours Faithfully: an Everyday Story of Formality" / 119kb PDF
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.
Click here for an 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".
2003
"Static
Verification and Extreme Programming" / 252kb PDF
Peter Amey and Roderick Chapman. Proceedings of
the ACM SIGAda Conference, December 2003.
Click here for an 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" / 225kb PDF
Roderick Chapman, Janet Barnes, and Brian Dobbing.
Submitted as a position paper to the 2nd NASA/FAA Object Oriented
Technology in Aviation Workshop.
Click here for an 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.
"High
Integrity Ravenscar" / 53kb PDF
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.
Click here for an 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.
"Automation
for Exception Freedom Proofs"
Bill J. Ellis and Andrew Ireland, Heriot-Watt University
18th IEEE International Conference on Automated Software Engineering
(ASE'03), 2003.
Click here for an abstract...
Run-time errors are typically seen as unacceptable within
safety and security critical software. The SPARK approach
to the development of high integrity software addresses the
problem of run-time errors through the use of formal verification.
Proofs are constructed to show that each run-time check will
never raise an error, thus proving freedom from run-time exceptions.
Here we build upon the success of the SPARK approach by increasing
the level of automation that can be achieved in proving freedom
from exceptions. Our approach is based upon proof planning
and a form of abstract interpretation.
2002
"Closing the loop
– The Influence of Code Analysis on Design" / 214kb PDF
© 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
Click here for an 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.
"Industrial
Strength Exception Freedom" / 231kb PDF
Roderick Chapman and Peter Amey, Praxis. Proceedings of ACM
SigAda 2002.
Click here for an 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.
2001
"A Language
for Systems not just Software" / 271kb PDF
Peter Amey, Praxis, September 2001.
This paper was presented at the ACM SigAda 2001 conference,
in Minneapolis, USA.
"SPARK :
a state-of-the-practice approach to the Common Criteria implementation
requirements" / 223kb PDF
Rod Chapman, Praxis. Presented at the 2nd International Common
Criteria Conference, Brighton, UK, July 2001
Click here for an 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.
"Logic versus
Magic in Critical Systems" / 315kb PDF
© 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.
Click here for an 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. This paper is one of
the keynote presentations at this year's Ada-Europe conference.
2000
"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.
"Cost-Effective Approaches to Safetify Safety-Critical
Regulatory Requirements"
James Sutton, Lockheed Martin, Presented in workshop session
at SigAda 2000.
"Industrial Experience with SPARK" / 234kb PDF
Dr. Roderick Chapman, Praxis High Integrity Systems Limted.
Presented at ACM SigAda 2000 conference.
Click here for an 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.
1999
"Re-engineering
a Safety-Critical Application with SPARK95 and GNORT" / 67kb PDF
Roderick Chapman and Robert Dewar,
Lecture
Notes in Computer Science 1622
Reliable Software Technologies – Ada-Europe '99
(c) Springer-Verlag 1999.
Click here for an 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.
1995
"Breaking Through the V and V Bottleneck" / 255kb PDF
Martin Croxford and James Sutton. Presented at Ada Europe
1995,
Published by Springer-Verlag in "Lecture Notes in Computer
Science" Volume 1031, 1996.
Click here for an abstract...
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.