Validation method on protocol specification based on infinite automata

摘要

The present invention relates to a test method for a protocol specification based on finite automata, wherein there is a livelock state or a state set that does not return to the initial state by repeating infinitely only a deadlock state and a subset of states without any transition in the automata model. A safety test process to check whether the test is performed, a determinism test process to test the non-determinism in which two or more transitions exist due to the same action in any state of the automata model, and an input action and an output action at any state in the automata model. In order to test whether or not the condition is achieved, the statefulness verification process, which checks whether the automata satisfies the statefulness characteristic expressed by the logic of Modal mu-calculus, is performed through the model inspection technique, and the three successive actions in the automata model. Occurs in the specification For the behavior achievement test to check the performance of the finite automata-based protocol specification, which consists of the state achievement test process that checks whether the automata satisfies the behavior achievement characteristics expressed by the logical expression of Modal mu-calculus through the method of model inspection. Assay methods are disclosed.