Praxis High Integrity Systems - Publications and White Papers

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.

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. Praxis High Integrity Systems 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 Praxis High Integrity Systems 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.

Engineering the Tokeneer Enclave Protection Software

SafSec: Commonalities Between Safety and Security Assurance

Assurance Cases: how assured are you?

Formal Methods start to add up once again

How many lightbulbs does it take to change an Engineer?

How To Buy Consultancy and Survive

Static Verification and Extreme Programming

Engineering Software Systems for Customer Acceptance

On the Principled Design of Object-Oriented Programming Languages for High-Integrity Systems

White Box Software Development

Industrial Strength Exception Freedom

Electronic Safety Case: Challenges and Opportunities

Requirements Engineering: How Do You Know How Good You Are?