Automatic verification of fault tolerance using model checking

Model checking is a technique that can make a verification for finite state systems absolutely automatic. We propose a method for automatic verification of fault-tolerant systems using this technique. Unlike other related work, which is tailored to specific systems, we are aimed at providing a general approach to verification of fault tolerance. The main obstacle in model checking is state explosion. To avoid the problem, we design this method so that it can use SMV, a symbolic model checking tool. Symbolic model checking can overcome the problem by expressing the state space and the transition relation by Boolean functions. Assuming that a system to be verified is specified by guarded commands, we define a modeling language suited for describing guarded command programs and propose a translation method from the modeling language to the input language of SMV. We show the results of applying the proposed method to various examples to demonstrate the usefulness