| 摘要 |
PROBLEM TO BE SOLVED: To provide a formal verification method to verify the propriety of recovering from an abnormal state by itself. SOLUTION: When a circuit description is inputted (S1), a syntax analysis of the circuit description is carried out (S2) and then the circuit description is converted into a finite state machine of a Kripke structure (S3). A set of nodes that is reachable from an initial state set Vo is decided in a total set V as a set Vn of normal nodes (S4). Then a set of nodes which does not belong to the set Vn are decided in the set V as a set Vx of abnormal nodes (S5). It is retrieved whether it is possible or not to reach any one of nodes belonging to the set Vn from all nodes belonging to the set Vx (S6). If the retrieval result of the S6 is affirmed (S7), a fact that the recovering from an abnormal state is possible is notified (S8). If the retrieval result of the S6 is negated, a fact that the recovering from the abnormal state is impossible is notified (S9).
|
