University of Cambridge

Logic
&
Semantics

Attempting to reason about failures

By Cliff Jones (University of Newcastle upon Tyne)

I have been working with Ian Hayes and Michael Jackson trying to get a way of viewing failures in components as interference to a control program. My starting point is that many systems get more coherent specifications by pushing the initial specification out to the observable phenomena. Deriving the specification of the control system generates rely-conditions (cf. my earlier work on concurrency) about things beyond the control of the software. These rely-conditions do not in themselves make the overall system any safer but they at least form a clear record of the assumptions being made (which can be linked to some sort of hazard analysis). Our evolving ideas will be demonstrated on example(s) rather than with a worked out theory.