| 摘要 |
The invention concerns a device and verification method of the functional equivalence between an automaton entity (11) defining a group of automatons in finished condition (13) and a production code (15) generated from said automaton entity (11) by a production code generator (1), with the method including the following stages: - generate a reference code (19) from said automaton entity (11) using a generator (21) with a reference code different from said production code (15) generator (17), - define in another formal language at least one determined property (P), - supply said production and reference codes with identical input variables, with said production and reference codes supplying exit variables (S1, S2) resulting from said identical input variables, - compare said exit variables between one another according to said determined property (P) to prove the functional equivalence between said automaton entity (11) and said production code (15), - search using a formal method of proof (29) for values held by the exit variables (S1, S2) which place the aforementioned in default relative to at least one determined property (P), and - validate the functional equivalence between said automaton entity (11) and the production code when at least one determined property (P) of the aforementioned has been satisfied. |
