Formal specification of fault-tolerance and its relation to computer security
Dorian Weber · 1989
The techniques of formal verification are one means for gaining greater assurance of the correctness of software. These techniques require precise specification of the prop-erties to be assured. This paper formulates precise specifi-cations corresponding to the intuitive notions of “fault tol-erance ” and of “graceful degradation”. An analogy is con-structed between these fault-tolerance specifications and a particular class of specifications for computer security. On the basis of this analogy, it is argued that formal verifica-tion of fault tolerance will face some of the same problems, and benefit from some of the same solutions, as verification of security. 1