NDLI: Automatic verification of fault tolerance using model checking

Content Provider	IEEE Xplore Digital Library
Author	Yokogawa, T. Tsuchiya, T. Kikuno, T.
Copyright Year	2001
Description	Author affiliation: Dept. of Inf. & Math. Sci., Osaka Univ., Japan (Yokogawa, T.)
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 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.
Sponsorship	IEEE Comput. Soc. Tech. Committee onf Fault-Tolerant Comput.
Starting Page	95
Ending Page	102
File Size	743089
Page Count	8
File Format	PDF
ISBN	0769514146
DOI	10.1109/PRDC.2001.992685
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2001-12-17
Publisher Place	South Korea
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Fault tolerance Fault tolerant systems Informatics Electronic mail Mathematical model Explosions Design methodology State-space methods Boolean functions Availability
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Using MTBDDs for discrete timed symbolic model checking

First-order checking of ω - automata using MDGs

A Time Abstraction Method for Efficient Verification of Communicating Systems

Safety Verification of Asynchronous Consensus Algorithms with Model Checking

Formal checking of properties in complex systems using abstractions

Maximality-based symbolic model checking

Modular verification of a fault-tolerant active structure controller: an example

Modeling and Verification for Timing Satisfaction of Fault-Tolerant Systems with Finiteness

Implicit model checking: formal verification technique for large-scale discrete systems

Automatic verification of fault tolerance using model checking

Similar Documents

Using MTBDDs for discrete timed symbolic model checking

First-order checking of ω - automata using MDGs

A Time Abstraction Method for Efficient Verification of Communicating Systems

Safety Verification of Asynchronous Consensus Algorithms with Model Checking

Formal checking of properties in complex systems using abstractions

Maximality-based symbolic model checking

Modular verification of a fault-tolerant active structure controller: an example

Modeling and Verification for Timing Satisfaction of Fault-Tolerant Systems with Finiteness

Implicit model checking: formal verification technique for large-scale discrete systems

Automatic verification of fault tolerance using model checking