 |
|
|
|
Jul
2002
|
Effective Independent Safety Assessment
Authors: Keith
Harrison and Joanna Dawson
 Abstract
The purpose of an Independent Safety
Auditor (ISA) is to audit, assess and review processes used
in a project to show compliance to best and appropriate practice
and to assess the adequacy of the evidence. The main objective
of using an ISA in any project is to provide assurance that
a contractor considers and addresses safety issues. An ISA
needs to be convinced that the process captures, understands
and mitigates the hazards and identifies safety requirements
associated with a system. This is carried out by a review
of the safety analysis and support documents that leads to
the development of the system Safety Case. In addition, it
may be beneficial if the ISA conducts some independent analysis
to add to the safety evidence or assist in the understanding
of the system and its properties. This paper describes the
role of the ISA as used on a major UK MoD Procurement. It
describes the use of independent analysis using creative thinking
to develop a hazard model that provides understanding of the
system level hazards and their association with the subsystems.
View
PDF [361kb]
|
|
|
|
Closing the loop – The Influence of Code Analysis on
Design
Author: Peter
Amey
[Published in Lecture Notes in Computer Science 2361:
Reliable Software Technologies – Ada-Europe 2002
7th Ada-Europe International Conference, Vienna, Austria]
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.
View
PDF [213kb]
|
|
|
Mar
2002
|
Correctness By Construction: Better Can Also Be Cheaper
Author: Peter
Amey
[Published in CrossTalk Magazine, The Journal of Defence Software
Engineering]
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.
View
PDF [311kb]
|
|
|
Jan
2002
|
Correctness by Construction: Developing a Commercial Secure
System
Authors: Anthony
Hall and Roderick Chapman
[Published in IEEE Software, pp18-25.]
Abstract
When you buy a car, you expect it
to work properly. You expect the manufacturer to build the
car so that it's safe to use, travels at the advertised speed,
and can be controlled by anyone with normal driving experience.
When you buy a piece of software, you would like to have the
same expectation that it will behave as advertised. Unfortunately,
conventional software construction methods do not provide
this sort of confidence: software often behaves in completely
unexpected ways. If the software in question is security-
or safety-critical, this uncertainty is unacceptable. We must
build software that is correct by construction, not software
whose behavior is uncertain until after delivery. This article
describes how we applied this philosophy to the development
of a commercial secure system.
View
PDF [357kb]
|
|
|
Sep
2001
|
SPARK and Abstract Interpretation – A White Paper
Authors: Rod
Chapman
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 SPARK Examiner toolset. The aim
of this white paper is to dispel some of the common myths
and to avoid potential confusion with customers.
View
PDF [203kb]
|
|
|
Sep
2001
|
A Language for Systems not just Software
Author: Peter
Amey
Abstract
The specification and implementation
of software-intensive systems have generally been viewed as
separate processes with differing notations. There are good
reasons for trying to use notations capable of bridging the
gap between the two. The SPARK language was originally concerned
solely with providing an unambiguous subset of Ada that was
suitable for rigorous static analysis and formal verification.
Evolution of SPARK'S system of formal comments or annotations
has resulted in a language which now provides parallel descriptions
of required system behaviour and software implementation.
Analyses performed by the SPARK Examiner bind these parallel
descriptions together. The result, not foreseen by the original
designers of SPARK, is a language that can be used to describe
systems rather than just implement software.
View
PDF [270kb]
|
|
|
Aug
2001
|
Will it Work?
Authors: Jonathan
Hammond, Rosamund Rawlings, Anthony Hall
[Published in RE'01, the proceedings
of the 5th IEEE International Symposium on Requirements Engineering]
Abstract
This paper describes experiences
using Requirements Engineering (RE) to reduce the risk of
large heterogeneous distributed systems not working in their
intended environments. Industry is creating ever-larger systems
by integrating increasingly complex smaller systems. As a
result, systems integration is becoming a major, or even dominant,
risk in the production of systems such as an aircraft, railway
or telecommunications infrastructure. In this paper, we describe
some practical techniques we use for the RE of such integrated
systems. They aim to provide assurance, before development,
that the final integrated system will achieve its overall
requirements. We illustrate the techniques with case studies
drawn from their industrial application.
View
PDF [510kb]
|
|
|
Jul
2001
|
SPARK – a state-of-the-practice approach to the Common
Criteria implementation requirements
Authors: Rod
Chapman
[Presented at the 2nd International
Common Criteria Conference, Brighton, UK]
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.
View
PDF [222kb]
|
|
| |
Publications
page 1 | 2 | 3
| |
|
| |
© Website Content Praxis High Integrity Systems 2008
Normal
text Large
text
|
|
|
|
- 
