Patent ID: 7743351
Filing Date: 2010-06-22
Classification: G06F

Abstract:
1. A method of verifying the robustness of a model of a physical system, the method comprising the following steps: defining a first model of the physical system 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; defining in the formal language a determined property that must be satisfied by the model of the physical system; using a computer system executing formal proof software stored on computer-readable media to search automatically for a combination of input values that causes said determined property to fail relative to said first model; providing a diagnosis comprising sequences of input values in case said determined property fails relative to the first model; correcting the first model so that said determined property is verified to be true relative to the first model; defining in the formal language a second model of the physical system corresponding to the first model and enriched by a fault injection mechanism if no combination of input values that causes said determined property to fail is found and said determined property has already been verified to be satisfied relative to the first model; and using a computer system executing formal proof software stored on computer-readable media to search automatically for a combination of injected faults and/or input values that causes said determined property to fail relative to the second model.