SPECIFICATION VERIFICATION DEVICE, ITS METHOD AND RECORDING MEDIUM RECORDING SPECIFICATION VERIFICATION PROGRAM

摘要

PROBLEM TO BE SOLVED: To verify specifications of a large-scale state, transition machine without damaging completeness by converting a Boolean expression to a BDD (binary decision diagram) and judging that the state transition machine expressed by an initial state and a state transition relation expression satisfies the specifications expressed by a CTL expression. ;SOLUTION: From an input part 1, the Boolean expression for expressing the set of the candidates of an initial state, the Boolean expression for expressing state transition relation and the CTL expression for expressing the specifications to be satisfied by the state transition machine expressed by the initial state and the state transition relation expression are inputted. A conversion part 2 to the BDD converts the Boolean expressions into the BDD. The conversion part 3 of the CTL expression converts the CTL expression to a tree form. A verificatiop part 4 calculates the reverse image calculation and logical operation of the BDD and verifies that the state transition machine expressed by the initial state and the state transition relation expression satisfies the specifications expressed by the CTL expression.;COPYRIGHT: (C)1999,JPO