Using Data Consistency Assumptions to Show System Safety

Systems cannot usually be proved safe unless some failure assumptions are made. Here we prove that the water level in a generic boiler system is always within its safe range by assuming that device failures result in inconsistent readings. Key parts of our approach are a failure-reporting strategy that determines failures from consistency conditions, and a level-calculation strategy that gives a best estimate of boiler level in light of the reported failures. These strategies are generic and could be used in other safety-critical applications.