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.
An Application of Regular Temporal Logic to Verification of Fail-Safeness of a Comparator for Redundant System
Kazuo KAWAKUBO Hiromi HIRAISHI
IEICE TRANSACTIONS on Information and Systems
Publication Date: 1993/07/25
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Issue on VLSI Testing and Testable Design)
fail-safe, fault tolerance, formal verification, temporal logic,
Full Text: PDF(717.1KB)>>
In this paper we propose a method of formal verfication of fault-tolerance of sequential machines using regular temporal logic. In this method, fault-tolerant properties are described in the form of input-output sequences in regular temporal logic formulas and they are formally verified by checking if they hold for all possible input-output sequences of the machine. We concretely illustrate the method of its application for formal verification of fail-safeness with an example of a comparator for redundant system. The result of verification shows effectiveness of the proposed method.