Combining Tools for the Verification of Fault-Tolerant Systems
Author: Bettina Buth, Rachel Cardell-Oliver and Jan Peleska
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
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)