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.

This paper presents a general method for computing quantitative information about finite-state real-time systems. We have developed algorithms that compute exact bounds on the delay between two specified events and on the number of occurrences of an event in a given interval. This technique allows us to determine performance measures such as schedulability, response time, and system load. Our algorithms produce more detailed information than traditional methods. This information leads to a better understanding of system behavior, in addition to determining its correctness. The algorithms presented in this paper are efficiently implemented using binary decision diagrams and have been incorporated into the SMV symbolic model checker. Using this method, we have verified a model of an aircraft control system with 1015 states. The results obtained demonstrate that our method can be successfully applied in the verification of real-time system designs.

The goal of this paper is to propose a new symbolic model checking approach named time-space modal model checking, which could be applicable to verification of bit-slice microprocessor of infinite bit width and one dimensional systolic array of infinite length. A simple benchmark result shows the effectiveness of the proposed approach.

This paper describes an efficient symbolic model checking algorithm for verification of deadlock free property of high level robot control program called Task Control Architecture (TCA). TCA is a model of concurrent robot control processes. The verification tool we used is the Symbolic Model Verifier (SMV). Since the SMV is not so efficient for verification of liveness properties of many concurrent processes such as deadlock free property, we first described the deadlock free property by using safety properties that SMV can verify efficiently. In addition, we modify the symbolic model checking algorithm of the SMV so that it can handle many concurrent processes efficiently. Experimental measurements show that we can obtain more than 1000 times speed-up by these methods.

Recently, Burch et al. proposed symbolic model checking method to verify sequential machines formally. The method, which is based on logic function manipulation using binary decision diagram, can handle large sequential machines that cannot be handled by the conventional techniques. The expressive power of Computational Tree Logic (CTL), which was used by Burch et al., is not very powerful, for example, CTL cannot describe repetition of events. This papers shows an extension of the symbolic model checking algorithm to Branching time regular temporal logic (BRTL), which has been proposed by the authors as an improvement of CTL in terms of expressive power. The implemented verifier based on the proposed algorithm could verify behaviors of a microprocessor composed of approximately 1,600 gates and 68 flipflops.

In this paper we propose a method of formal verification of totally self-checking (TSC) properties of combinational circuits using logic function manipulation. We show that the problem of verification of TSC properties can be transformed to a satisfiability problem of decision functions formed from characteristic functions of a circuit's output code words. Then the problem can be solved using binary decision diagrams (BDD). Experimental results show the effectiveness of the proposed method.