A method of verifying the robustness of a model of an electronic system comprising a first and a second computer (112a, 112b) for controlling an aircraft engine, the method comprising the following steps:. defining a first model of the electronic system modeling said first and said second computer (112a, 112b) and an inter-computer back gear comprising contact wires for data exchanging between said first and said second computer (112a, 112b), said first model comprising a set of components (12a, 12b, 12c) and at least an input interface for the introduction of input values, said first model being defined in a formal language describing the behavior and the function of each of said components;. defining in the formal language a determined property that must be satisfied by modeling the electronic system;. searching automatically using a formal proof means of a combination of input values that puts at fault said determined property vis-à-vis the first model for verifying the truth of said determined property; defining in the formal language a second model corresponding to the first model enriched by a fault injection mechanism when said determined property is verified as being true for the first model; and. searching automatically using a formal proof means of a combination of fault injection and / or input values that puts at fault said determined property vis-à-vis the second model, said determined property being considered as being true relative to the second model when the formal proof means finds no combination of fault injection and / or input values that puts at fault said determined property and considering the modeling of the electronic system to be robust with respect to faults vis-à-vis said determined property when said determined property is verified as being true for the second model.. defining a first model of the electronic system modeling said first and said second computer (112a, 112b) and an inter-computer back gear comprising contact wires for data exchanging between said first and said second computer (112a, 112b), said first model comprising a set of components (12a, 12b, 12c) and at least an input interface for the introduction of input values, said first model being defined in a formal language describing the behavior and the function of each of said components;. defining in the formal language a determined property that must be satisfied by modeling the electronic system;. searching automatically using a formal proof means of a combination of input values that puts at fault said determined property vis-à-vis the first model for verifying the truth of said determined property; defining in the formal language a second model corresponding to the first model enriched by a fault injection mechanism when said determined property is verified as being true for the first model; and. searching automatically using a formal proof means of a combination of fault injection and / or input values that puts at fault said determined property vis-à-vis the second model, said determined property being considered as being true relative to the second model when the formal proof means finds no combination of fault injection and / or input values that puts at fault said determined property and considering the modeling of the electronic system to be robust with respect to faults vis-à-vis said determined property when said determined property is verified as being true for the second model.