IEICE TRANSACTIONS on Information
An Application of Regular Temporal Logic to Verification of Fail-Safeness of a Comparator for Redundant System
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E76-D No.7 pp.763-770
- Publication Date
- 1993/07/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Issue on VLSI Testing and Testable Design)
- 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
Kazuo KAWAKUBO, Hiromi HIRAISHI, "An Application of Regular Temporal Logic to Verification of Fail-Safeness of a Comparator for Redundant System" in IEICE TRANSACTIONS on Information,
vol. E76-D, no. 7, pp. 763-770, July 1993, doi: .
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/e76-d_7_763/_p
Copy
@ARTICLE{e76-d_7_763,
author={Kazuo KAWAKUBO, Hiromi HIRAISHI, },
journal={IEICE TRANSACTIONS on Information},
title={An Application of Regular Temporal Logic to Verification of Fail-Safeness of a Comparator for Redundant System},
year={1993},
volume={E76-D},
number={7},
pages={763-770},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={July},}
Copy
TY - JOUR
TI - An Application of Regular Temporal Logic to Verification of Fail-Safeness of a Comparator for Redundant System
T2 - IEICE TRANSACTIONS on Information
SP - 763
EP - 770
AU - Kazuo KAWAKUBO
AU - Hiromi HIRAISHI
PY - 1993
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E76-D
IS - 7
JA - IEICE TRANSACTIONS on Information
Y1 - July 1993
AB - 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.
ER -
English
