Automatic verification of fault tolerance using symbolic model checking

摘要

We propose a model checking method for automatic verification of fault tolerance of systems. We assume that a system to be verified is given in the form of a guarded-command program. This method uses a symbolic model checking tool called SMV (Symbolic Model Verifier). Although it has been widely applied to hardware systems, it is rarely reported to apply to software systems. In this paper we define a modeling language suited for describing guarded command programs, and then we propose a translation method from the modeling language to the input language of SMV. Finally we apply the proposed method to an example in the literature to verify fault tolerance of the system.