Example IEC 61508 Safety Case: Formal Models


SIL4SIL3 Certified
 
iso9001 certified
iso14001 certified
 

Deep Life Ltd use both Matlab for formal specification and modelling, and this fits 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 Open Revolution rebreather project.

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.

Feedback on support issues should be sent to support@deeplife.co.uk

acrobat reader

User manual for the DL 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 Quick Start Guide: Link (click here)


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 histor, 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). DL are preparing for publication the GF and VPM . 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.