IEC 61508 Safety Case: Formal Models

Deep Life Group, including Open Safety Equipment Ltd, use both Matlab for formal specification and modelling, fitting well with the use of SPARK Ada and other coding tools. Matlab operates with unbounded systems, such as those with analogue sensors, and is easy to follow. For those reasons, we have chosen Matlab for the specification modelling for the rebreather development, resulting in the six rebreather models produced by Open Safety Equipment Ltd (OSEL). All rebreather code used by OSEL is written in SPARK Ada, a language used for the most onerous safety applications, including nuclear reactor control, Heathrow's air traffic control, the European Fighter Project and others.

The models published below are believed to be the most detailed available for a rebreather. If there is a material feature not represented, or a phenomenon not caputured, please let us know.

acrobat reader User manual for the Comprehensive Rebreather Model(691KB)
This is the user manual for the Verification model below.
A quick start guide is also available, from the Rebreather-World library, written by one of its users: available from in 2014 - use the WebArchive on to access.

Deep Life's Comprehensive Rebreather Verification Model
Rev 3e: Last update 6/3/2008 (488KB)

This rebreather model is believed to be the most detailed and exact rebreather verification model in existence, modelling the environment, the rebreather, sensors and actuators.
The model is used to validate each part of the design and its implementation: that is every part of the design is formally verified.
The model is also used in in accident investigation to reduce the list of plausible causes left from filtering the FMECA Vol 6 list faults with the evidence available. See the Readme file for revision history, and examples of use.

Reference Verification Model for Buhlmann ZH-16A Decompression Algorithm with GUI (300KB)
MatLAB R14 and Simulink code, with documentation and a GUI, for the Reference Model for the ZH-16A Decompression Algorithm, with extra compartment for He (Compartment 1b). These are reference models and should be used for that purpose only (that is, independent code verification).

To use: Unzip, Start MatLab R14, click on main_RB_TB.m and run it (F5). You should now see a dive computer like GUI. Enter a profile using Manual mode or reading a profile (under Depth), then RUN, PAUSE, change to Deco (under Depth), RUN to get deco profile. See graphs under Profile Figure.