 |
|
|
|
May
2001
|
Logic versus Magic in Critical Systems
Author: Peter
Amey
[Published in Lecture Notes in Computer Science 2043
Reliable Software Technologies – Ada-Europe 2001
6th Ada-Europe International Conference, Leuven, Belgium]
 Abstract
A prevailing trend in software engineering
is the use of tools which apparently simplify the problem
to be solved. Often, however, this results in complexity being
concealed or "magicked away". For the most critical of systems,
where a credible case for safety and integrity must be made
prior to there being any service experience, we cannot tolerate
concealed complexity and must be able to reason logically
about the behaviour of the system. The paper draws on real-life
project experience to identify some historical and current
magics and their effect on high-integrity software development;
this is contrasted with the cost and quality benefits that
can be made from taking a more logical and disciplined approach.
View
PDF [314kb]
|
|
|
|
Industrial Experience with SPARK
Author: Roderick
Chapman
[published for SIGAda 00, Laurel, MD, USA]
Abstract
This paper considers a number of
large, real-world projects that are using SPARK – an
annotated sublanguage of Ada that is appropriate for the development
of high-integrity systems. Three projects are considered in
some detail where SPARK has made a contribution to meeting
the most stringent software engineering standards. The projects
are the Ship/Helicopter Operational Limits Instrumentation
System (UK Interim Defence Standard 00-55), the MULTOS CA
(a high-security system developed to the standards of ITSEC
level E6), and the Lockheed C130J Mission Computer (DO-178B
Level A). A less successful project is also described. The
lessons learnt from these projects show that SPARK offers
a cost-effective approach for the construction of high-integrity
software when it is deployed judiciously within an appropriate
software development process.
View
PDF [233kb]
|
|
|
Aug
2000
|
Is Proof More Cost Effective than Testing?
Authors: Steve
King, Jonathan Hammond, Rod Chapman and Andy Pryor
[IEEE Transactions on Software Engineering, Vol 26, no 8]
Abstract
This paper describes the use of
formal development methods on an industrial safety-critical
application. The Z notation was used for documenting the system
specification and part of the design, and the SPARK 1 subset
of Ada was used for coding. However, perhaps the most distinctive
nature of the project lies in the amount of proof that was
carried out: proofs were carried out both at the Z level – approximately 150 proofs in 500 pages – and at the SPARK code
level – approximately9,000 verification conditions generated – and discharged. The project was carried out under UK Interim
Defence Standards 00-55 and 00-56, which require the use of
formal methods on safety-critical applications. It is believed
to be the first to be completed against the rigorous demands
of the 1991 version of these standards. The paper includes
comparisons of proof with the various types of testing employed,
in terms of their efficiency at finding faults. The most striking
result is that the Z proof appears to be substantially more
efficient at finding faults than the most efficient testing
phase. Given the importance of early fault detection, we believe
this helps to show the significant benefit and practicality
of large-scale proof on projects of this kind.
View
PDF [656kb]
|
|
|
Oct
1995
|
Breaking Through the V & V Bottle Neck
Authors: Martin
Croxford, James Sutton
[Presented at Ada in Europe]
Abstract
With conventional methods of performing
verification and validation – heavily reliant on testing performed
late in the software production process -the late detection
of errors adds substantially to project costs and delays in
delivery, and introduces significant risks. This paper presents
a method of software development aimed at "correctness by
construction", which greatly attenuates these problems. The
process described here has been applied successfully to the
development of avionic software for the new C-130J ("Hercules")
aircraft.
View
PDF [254kb]
|
|
| |
Publications
page 1 | 2
| 3 | |
|
| |
© Website Content Praxis High Integrity Systems 2008
Normal
text Large
text
|
|
|
|
- 
