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 captured, please let us know.
User manual for the Comprehensive Rebreather Model
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.
Deep Life's Comprehensive Rebreather Verification Model
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 accident investigation to reduce the list of plausible causes left from filtering the FMECA Vol 6 list faults with the evidence available.
Reference Verification Model for Buhlmann ZH-16A Decompression Algorithm with GUI
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).