Whitepapers & publications

The traditional correctness semantics of preconditions and postconditions is not suitable for concurrent programming. This article outlines a new semantics for preconditions and postconditions which applies equally well in concurrent and sequential contexts and permits a flexible use of contracts for specifying the mutual rights and obligations of clients and suppliers while preserving the potential for parallelism. We argue that the new semantics is a generalisation of the traditional correctness semantics. We also propose a proof technique for concurrent programs which supports proofs - similar to those for traditional non-concurrent programs - of partial correctness and loop termination in the presence of asynchrony.

Full print version is available here

The contract-based SCOOP model enables the construction of object-oriented concurrent applications with little more effort than sequential ones. The model provides strong safety guarantees: mutual exclusion and atomicity at the routine level, and FIFO scheduling of clients' calls. Unfortunately, in the original proposal of the model these guarantees come at a high price: they entail locking all the arguments of a feature call; in most cases, the amount of locking is higher than necessary. We propose two refinements of the access control policy for SCOOP: a type-based mechanism to optimise locking, and a lock passing mechanism for safe handling of complex synchronisation scenarios with mutual locking of several separate objects. These refinements increase the expressive power of the model, give programmers more control over the computation, and enable more potential parallelism, thus reducing the risk of deadlock.

Full print version is available here

The Tokeneer ID Station (TIS) project, carried out by Altran Praxis 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 Altran Praxis, 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.

Many systems, particularly in the military domain, must be certified or accredited by both safety and security authorities. Current practice argues safety and security accreditations separately. A research project called SafSec has been investigating a combined approach to safety and security argumentation, and has shown that there can be practical benefits in performing a combined analysis and documenting a combined argument for both safety and security.

This paper proposes an approach to system assurance that acknowledges the commonality between different threads of safety, security and reliability, reduces duplicated work and can be supported by web-enabled tools. It provides assurance that systems will meet with regulators and budget holders' approval.

We discuss some of the problems with the current means of proving assurance and how the best practices in the safety, security and reliability domains could benefit from being brought together within a suitable framework to achieve a single, unified assurance case.

We offer up a solution by way of an eDependabilityCase (eDC) tool, working within a single integrated framework, to develop and present an assurance case.

Aircraft designers use mathematics to model the complex systems of lift and thrust needed to keep an Airbus in the sky. Bridge designers use mathematics to assess the stresses on the materials from which they can build bridges. Regulators of these industries demand that designers use rigorous methods. Formal methods is the equivalent mathematical foundation for software. It is the use of mathematics to specify, model, develop and reason about computing systems.

Here's a conundrum for those readers who are about to make a change to the way you do things in your Engineering Design department. On the one hand, engineers don't like change. On the other hand, engineers are perfectionists who are always looking for better ways of doing things. How can we plot a course between these inconsistencies?

When a Director “gets in the consultants”, do they get what they expected? Do they get value for money? If they are educated, experienced, careful buyers then the answer is usually “yes”. But many buyers don’t understand that different consulting firms have different agendas, skills and approaches.

This article explores some of the pitfalls that await the unwary buyer of consultancy and explains how to turn a potentially disappointing experience into a win-win for both parties.

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.

Building a software system is a well-understood problem with a wide range of solutions, each suitable for some classes of system but not for others. The commercial success of a software system, however, depends on its acceptance by the customer. Therefore, the developer must demonstrate that a system is fit for its purpose. A common view is that following a specified software or systems development process is adequate for this purpose. However, as software and safety standards move from a prescriptive to goal-oriented form, this demonstration of fitness will become better tailored to each system.

In this paper we examine how existing processes and products can be used to build an evidence-based case for high-assurance system acceptance. We draw on our own experience of developing and delivering such systems, and make practical recommendations for improving acceptance rates. We show how existing technologies and tools can support this process.

Systems for which failure can cause loss of life, injury, environmental damage, or financial loss are known as high integrity systems. These are all systems for which the cost of failure is not tolerable or affordable.

As high integrity systems become more prevalent in our every day lives the number of people involved in the production of these systems has increased, bringing popular technologies from the mainstream software community to the world of high integrity systems.

Object-Oriented Technology (OOT) is seen by many as the current "silver bullet" of software development; it is popular in the software community at large and benefits from a wide range of tool support. In looking to embrace this popular technology within the high integrity sector it is crucial that we ensure that the underlying design principles for high integrity systems are not compromised.

This article attempts to debunk the populist view that building high quality software is difficult and costly, and that having software systems that crash is an acceptable state of affairs. The technology to build predictable reliable software systems exists today. Principled engineering judgment can be used to tailor software development so that quality can be built in with cost in mind – this is particularly the case with safety critical systems, where the application of standards can force an unnecessarily rigorous approach for little proven benefit.

This article explores the general poor quality of software "in the large", the public's (and the industry's) view that this is in some way acceptable, and then presents some real case studies which show how quality can be built in without the need to invest in overweight tools and technologies.

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.

This paper describes the use of electronic formats for safety cases to meet the requirements of a number of military and civil standards. The challenge to safety engineers is to produce safety cases that are quickly readable, intelligible and auditable even when a large amount of material is required. We describe the problems in developing complex safety cases using traditional development methods and the opportunities to address these problems by the development of an electronic safety case.

We then describe an example eSafety Case and how this can be used to manage a safety programme and to produce a safety case that will meet the requirements of the certification authorities.

Organisations are seeking to improve the way they undertake engineering activities. There are numerous ways of doing this, one of which is to undertake an on-going process, or capability, enhancement activity. Altran Praxis Limited provides support for such activity based primarily around the REVEAL ® requirements engineering method. By providing customised training and coaching in REVEAL ®, we aim to build up a long-term sustainable skill in the client’s organisation.

Both Altran Praxis Limited and the client need to measure the effectiveness of the knowledge transfer. To meet this need we have developed the REVEAL ® Competency and Assessment scheme. This paper discusses the steps in this process and shares some experiences of using the scheme both in-house and with two major clients.

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.

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.

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.

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.

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.

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.

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.

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 Altran Praxis using SPARK to meet the requirements of ITSEC E6.

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.

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.

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.

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.