The device and method of verification of the equivalence between a functional entity of automata and a code of production.

摘要

The present invention relates to a device and a method of checking the functional equivalence between an entity of the programmable logic controllers (11) defining a set of automata to a finite state (13) and a code for the production (15) representing said entity of the programmable logic controllers (11) and is generated on the basis of the said arrangement of the programmable logic controllers (11) by a generator (17) of the code of production, the method comprising the following steps: - generate a reference code on the basis of the said arrangement of the programmable logic controllers (11) and representing said entity by a generator (21) of the reference code, different from said generator (17) of the code of production (15), - created in a formal language, of a code that is common (35) comprising the production of reference, a producer (37) of the input variables (e1, e2) intended to supply the production and reference to the input variables which are identical, and an output interface (39) intended to supply of the output variables (s1, s2), - define in a formal language, at least one property (p) is determined that the said common code must satisfy in order to demonstrate the equivalence between the said arrangement of functional units (11) and the code of production (15), - find by means of a formal proof (29) of the values taken by the variables of the outputs (s1, s2) which a fault, the said at least one property (p), - validate the equivalence between the said arrangement of functional units (11) and the code for the production (15) when the said at least one property (p) is determined is satisfied.