For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
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
Publication Date: 2002/11/01
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)>>
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.