A method for verifying traceability of first code instructions in a procedural programming language generated from second code instructions in a modelling language, comprising the application by data processing means of a piece of equipment of steps for: (a) Syntax analysis: ∘ of the first code instructions according to a library of said procedural programming language so as to generate an abstract syntax tree, AST, of the first instructions, and ∘ of the second code instructions according to a library of said modelling language so as to generate a modelling tree, MDT, of the second instructions, said modelling tree representing the nesting structure and the functional links of the model formed with the second instructions; (b) A semantic analysis: ∘ of the abstract syntax tree, AST, of the first instructions so as to identify patterns representative of elementary functional blocks of the first instructions so as to identify said functional blocks in the first instructions; ∘ of the modelling tree, MDT, of the second instructions so as to identify properties characteristic of elementary functional blocks of the second instructions so as to identify said functional blocks in the second instructions; each elementary functional block constituting a logical unit determining one or several output parameters from one or several input parameters and from a possible internal state; characterized in that it further comprises the application by the data processing means of a step of: (c) Pairwise matching of the identified elementary functional blocks and of interactions between said blocks, and confirming traceability of the first code instructions only if: ∘ for each block of the first instructions, there exists a functionally equivalent block of the second instructions; ∘ for each block of the second instructions, there exists a functionally equivalent block of the first instructions; and ∘ for each interaction between two blocks of the second instructions, there exist the same interaction between the two corresponding blocks of the first instructions, said interactions between blocks of the second instructions corresponding to partial order relations representing the time dependency of the two blocks. (a) Syntax analysis: ∘ of the first code instructions according to a library of said procedural programming language so as to generate an abstract syntax tree, AST, of the first instructions, and ∘ of the second code instructions according to a library of said modelling language so as to generate a modelling tree, MDT, of the second instructions, said modelling tree representing the nesting structure and the functional links of the model formed with the second instructions; ∘ of the first code instructions according to a library of said procedural programming language so as to generate an abstract syntax tree, AST, of the first instructions, and ∘ of the second code instructions according to a library of said modelling language so as to generate a modelling tree, MDT, of the second instructions, said modelling tree representing the nesting structure and the functional links of the model formed with the second instructions; (b) A semantic analysis: ∘ of the abstract syntax tree, AST, of the first instructions so as to identify patterns representative of elementary functional blocks of the first instructions so as to identify said functional blocks in the first instructions; ∘ of the modelling tree, MDT, of the second instructions so as to identify properties characteristic of elementary functional blocks of the second instructions so as to identify said functional blocks in the second instructions; each elementary functional block constituting a logical unit determining one or several output parameters from one or several input parameters and from a possible internal state; ∘ of the abstract syntax tree, AST, of the first instructions so as to identify patterns representative of elementary functional blocks of the first instructions so as to identify said functional blocks in the first instructions; ∘ of the modelling tree, MDT, of the second instructions so as to identify properties characteristic of elementary functional blocks of the second instructions so as to identify said functional blocks in the second instructions; ∘ for each block of the first instructions, there exists a functionally equivalent block of the second instructions; ∘ for each block of the second instructions, there exists a functionally equivalent block of the first instructions; and ∘ for each interaction between two blocks of the second instructions, there exist the same interaction between the two corresponding blocks of the first instructions, said interactions between blocks of the second instructions corresponding to partial order relations representing the time dependency of the two blocks.