An Application of Regular Temporal Logic to Verification of Fail-Safeness of a Comparator for Redundant System

Kazuo KAWAKUBO  Hiromi HIRAISHI  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E76-D   No.7   pp.763-770
Publication Date: 1993/07/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Issue on VLSI Testing and Testable Design)
Category: 
Keyword: 
fail-safe,  fault tolerance,  formal verification,  temporal logic,  

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




Summary: 
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.