Verifying Fault Tolerance of Concurrent Systems by Model Checking

Tomoyuki YOKOGAWA  Tatsuhiro TSUCHIYA  Tohru KIKUNO  

IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E85-A   No.11   pp.2414-2425
Publication Date: 2002/11/01
Online ISSN: 
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on Concurrent System Technology and Its Application to Multiple Agent Systems)
symbolic model checking,  fault tolerance,  SMV,  concurrent system,  guarded command,  

Full Text: PDF(506.7KB)>>
Buy this Article

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 concurrent systems using this technique. Unlike other related work, which is tailored to specific systems, we are aimed at providing an approach that can be used to verify various kinds of systems against fault tolerance. The main obstacle in model checking is state explosion. To avoid the problem, we design this method so that it can use a symbolic model checking tool called SMV (Symbolic Model Verifier). 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 modeled as a guarded command program, we design a modeling language 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 feasibility of the method.