Refinement and dependable systems

Dependable systems must often detect, recover from, and tolerate faults. A common problem in the behavioural specification of such systems is that one cannot specify a response to faults without also specifying that faults must be able to occur, even though non-faulty systems are acceptable. Our solution is to adopt modal process logic, which allows one to distinguish between events of a specification that must be implemented and those that may be implemented. We describe the problem and illustrate the application of modal process logic to the verification of an industrial failure-recovery protocol