Verifying Fault Tolerance of Concurrent Systems by Model Checking
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E85-A No.11 pp.2414-2425
- Publication Date
- 2002/11/01
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Section on Concurrent System Technology and Its Application to Multiple Agent Systems)
- Category
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Tomoyuki YOKOGAWA, Tatsuhiro TSUCHIYA, Tohru KIKUNO, "Verifying Fault Tolerance of Concurrent Systems by Model Checking" in IEICE TRANSACTIONS on Fundamentals,
vol. E85-A, no. 11, pp. 2414-2425, November 2002, doi: .
Abstract: 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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e85-a_11_2414/_p
Copy
@ARTICLE{e85-a_11_2414,
author={Tomoyuki YOKOGAWA, Tatsuhiro TSUCHIYA, Tohru KIKUNO, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Verifying Fault Tolerance of Concurrent Systems by Model Checking},
year={2002},
volume={E85-A},
number={11},
pages={2414-2425},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={November},}
Copy
TY - JOUR
TI - Verifying Fault Tolerance of Concurrent Systems by Model Checking
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 2414
EP - 2425
AU - Tomoyuki YOKOGAWA
AU - Tatsuhiro TSUCHIYA
AU - Tohru KIKUNO
PY - 2002
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E85-A
IS - 11
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - November 2002
AB - 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.
ER -
English
