| 摘要 |
PROBLEM TO BE SOLVED: To automatically synthesize a state transition from an operation rule, simultaneously output a verification result by a model inspection device about whether the synthesized state transition is not contradictory to an operation scenario, and automatically produce a verification model and a verification formula for model inspection. SOLUTION: A state transition design support apparatus includes an automaton production unit for converting an operation rule input from a user into an automaton format; an automaton synthesis unit for obtaining a product of the automaton to output it as a synthetic automaton; a verification model/verification formula production unit for producing a verification model based on each operation scenario input from the user and the synthetic automaton, and producing a verification formula for checking that the operation scenario is executed to the end and operation prohibited by the synthetic automaton is absent; and an inspection unit for performing model inspection using the verification model and the verification formula. COPYRIGHT: (C)2011,JPO&INPIT
|
