Checking the robustness of a model of a physical system

A system for verifying the robustness of a model of a physical system, the system comprising:

• a first model defining the physical system and comprising a set of components and at least one input interface for inserting input values, said first model being defined in a formal language describing the behavior and the function of each of said components:
• a predetermined property defined in the formal language that must be satisfied by the model of the physical system;
• a computer executing formal proof software for searching automatically for a combination of input values that causes said determined property to fail relative to the first model;
• means for providing a diagnosis comprising sequences of input values in case said determined property fails relative to the first model;
• means for correcting the first model so that said determined property is verified to be true relative to the first model;
• a second model of the physical system defined in the formal language, the second model corresponding to the first model enriched by a mechanism for injecting faults, said second model being defined if the computer executing formal proof software finds no combination of input values that causes said determined property to fail and said determined property has already been verified to be satisfied relative to the first model;
• and
• a computer executing formal proof software for searching automatically for a combination of injected faults and/or input values that causes said determined property to fail relative to the second model.