Ada Europe
Conference Home Page
University of York

Tutorial

Correctness by Construction—A Manifesto for High Integrity Engineering

Peter Amey & Neil White, Praxis High Integrity Systems
Monday June 20th, morning

Two of the major recurring issues in systems and software engineering are unacceptably high defect rates, and lack of ability to make changes over a significant period of time in a reliable manner. These issues frequently cause major impact on the usability and maintainability of systems, and this impact becomes intolerable when components of the system become unmaintainable, or when high levels of security accreditation or safety certification must be achieved.

This tutorial presents the Correctness by Construction high integrity approach to systems and software engineering. Correctness by Construction is based on a set of principles, distilled from practical project experience, to realize systems and software engineering outputs with very low defect rate and very high resilience to change. These principles can be applied most effectively to new developments and upgrades. However some of the same principles can also be applied retrospectively to improve the maintainability and upgradability of existing systems.

Topics covered in the tutorial include:

  1. The challenges that we face
  2. How Correctness by Construction addresses the challenges
    1. Validating the concepts of operation
    2. Risk-directed requirements engineering
    3. Formal specification
    4. Rigorous design and implementation based on static analysis
    5. Making the case for safety and security
    6. Maintaining correctness through long-term upgrades
  3. Correctness by Construction in action - project examples

Why should you attend this tutorial?

The challenge of producing software that has an acceptably-low defect rate is hard enough. To do so under time and budget pressures is harder still. Yet the pressures grow ever stronger and the trust we place in software-intensive systems continues to rise. There is a pressing need to find ways of producing high-integrity software at an acceptable cost.

Over the past 16 years, Praxis has evolved a practical approach to software development which delivers exceptionally low defect rates with very high productivity. The approach eschews the use of fashionable technologies and silver bullets preferring an engineering approach which favours error prevention and relentless error elimination at every stage of development. The result is a development process that generates a continuous forward flow from requirements to implementation.

The tutorial will describe how this approach, which has come to be called Correctness by Construction works and how it has been applied to significant, real-world projects.

Presenter

Peter Amey is an aeronautical engineer by original professional training. He served as an engineering officer in the Royal Air Force and spent several years at the Boscombe Down test establishment working on the certification of aircraft armament systems. Peter joined Program Validation Limited in 1992 to develop SPARK and the SPARK Examiner and continues that work today with Praxis High Integrity Systems. As well developing SPARK he has used it on major programmes including Tornado, Eurofighter and the Lockheed C130J. Peter, now Chief Technical Officer at Praxis, teaches SPARK and Ada on a regular basis and has lectured widely on the development of critical systems.


The organizers thank the supporters of the conference


Praxis High Integrity Systems
Silver Software

Ada Conference Home Page


Last Changed: Wed Jun 15 10:01:57 2005
Contents of this page : Ian Broster