School of Computer Science The University of Adelaide Australia
Computer Science Home
About the School
Staff Only
text zoom: S | M | L

School of Computer Science
Innova21 Building
SA 5005

Telephone: +61 8 8313 5586
Facsimile: +61 8 8313 4366

You are here: Computer Science > Courses > High Integrity Software Engineering

High Integrity Software Engineering


Software is increasingly being used in systems of a critical nature, in particular in safety critical systems, where failure of the software can lead to catastrophic effects, including injury or death to humans, and harm to the environment. Examples of software-based safety critical systems include: fly-by-wire avionics; drive-by-wire technology in cars; implantable defibrillators; train control and train signalling systems; and computer-aided emergency dispatch systems. Increasingly software is replacing hardware or human operators, allowing for more complex and (arguably) cost effective solutions, but at the same time leading to a system that is more difficult to provide assurance for. Because of this, the development of software for safety critical systems requires engineering techniques above and beyond standard software engineering methods. We refer to the discipline of developing safety critical software as high-integrity software engineering.

This course will cover a number of practical techniques used in high-integrity software engineering. The course will include hazard and risk analysis techniques, including fault tree analysis, event tree analysis, failure modes and effects analysis and hazard and operability studies, which are used in determining the critical components in the system. We introduce a range of development techniques that can then be applied to developing critical software components, thus achieving higher levels of assurance. Techniques covered include: formal specification using the Z language; defensive programming, design by contract, static analysis and the SPARK Ada safe programming languages; and formal verification using both model checking in SPIN and theorem proving in Isabelle/HOL. These techniques are all prescribed by a variety of international standards for the development of safety critical systems, and most have been applied in large scale industry projects.

Course Outline

Topics covered in this course include:
  • Hazard and risk analysis
    • Fault Tree Analysis
    • Event Tree Analysis
    • HAZOP
    • Failure Mode and Effect Analysis
    • ALARP
    • Safety Integrity Levels
  • Formal Specification
  • Model Checking
  • Rigorous Software Development
    • Static Analysis
    • Design by Contract
    • Safe programming language subsets
  • Formal Verification

Course Offerings

North Tce, Adelaide