Combining Tools for the Verification of Fault-Tolerant Systems

Author: Bettina Buth, Rachel Cardell-Oliver and Jan Peleska

Abstract:
In this article, we describe an approach for the tool-supported development and verification of fault-tolerant systems according to the invent&verify paradigm. Our method is based on the CSP (Communicating Sequential Processes) specification language. It allows to express the desired properties of a system as implicit specifications (assertions about traces and refusals), explicit specifications (CSP process terms), refinement relations or combinations of these three description formalisms. From our experience with industrial verification projects, this possibility to choose between different specification paradigms according to the specific needs of each development step is essential to cope with large-scale formal development and verification projects. Each top-down development step according to the invent\&verify paradigm introduces a verification obligation whose type depends on the specification techniques applied for the different components involved in the step. We describe several strategies optimised for discharging specific forms of these obligations typically arising during a development. Application of these strategies is supported by three verifications tools: HOL is used to develop generic theories and apply them in strategies applicable for the verification of implicit specifications. FDR is used for the verification of refinement relations between CSP processes. PAMELA/PVS is applied for the verification of implicit assertions stated for explicit sequential processes. The main objective of this article is to show how these different specification formalisms and associated verification support tools can be most effectively combined to cope with complex fair-sized developments. Our approach is illustrated by means of a case study concerning the development of a fault-tolerant dual computer system.

compressed poscript file (149KB)