An Application of Regular Temporal Logic to Verification of Fail-Safeness of a Comparator for Redundant System (Special Issue on VLSI Testing and Testable Design)

スポンサーリンク

概要

• 論文の詳細を見る

• In this paper we propose a method of formal verification 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.

• 社団法人電子情報通信学会の論文
• 1993-07-25

著者

• KAWAKUBO Kazuo

  Faculty of Engineering, Fukuyama University

• Hiraishi Hiromi

  Faculty Of Engineering Kyoto Sangyo University

• Kawakubo Kazuo

  Faculty Of Engineering Fukuyama University

関連論文

• Formal Verification of Totally Self-Checking Properties of Combinational Circuits
• An Application of Regular Temporal Logic to Verification of Fail-Safeness of a Comparator for Redundant System (Special Issue on VLSI Testing and Testable Design)
• Temporal Verification of Real-Time Systems
• Towards Verification of Bit-Slice Circuits : Time-Space Modal Model Checking Approach
• Symbolic Model Checking of Deadlock Free Property of Task Control Architecture(Special Issue on Test and Verification of VLSI)

スポンサーリンク