Checking the robustness of a model of a physical system

• US 7,743,351 B2
• Filed: 05/05/2005
• Issued: 06/22/2010
• Est. Priority Date: 05/05/2004
• Status: Active Grant

• Current Assignee: Safran Aircraft Engine Company
• Original Assignee: Hispano Suiza SA (Safran SA)
• Inventors: Croix Marie, Marc, Granier, Hugues, Bregaint, Christian, Tonnelier, Philippe
• Primary Examiner(s): Chiang; Jack
• Assistant Examiner(s): Memula; Suresh
• Application Number:
  US11/122,109
• Publication Number:
  US 20050262457A1
• Time in Patent Office: 1,874 Days
• Field of Search: 716/5
• US Class Current: 716/106
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

The invention provides a system and a method for 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; defining in the formal language a second model corresponding to the first model and enriched by a fault injection mechanism; and using formal proof means to search automatically for a combination of injected faults and/or input values that causes said determined property to fail.

Claims

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.

2. A method according to claim 1, wherein the fault injection mechanism comprises injecting at least one fault into the second model via a fault input interface.

3. A method according to claim 2, wherein the fault injection mechanism further comprises a description in the formal language of at least one effect of said at least one fault on the function or the behavior of each of the components of said physical system.

4. A method according to claim 1, wherein the determined property is considered as being true relative to the second model when the formal proof software can find no combination of injected faults and/or input values that causes said determined property to fail.

5. A method according to claim 4, wherein the model of the physical system is considered as being robust relative to said determined property.

6. A method according to claim 1, wherein the determined property is considered as being false relative to the second model when the formal proof software finds at least one combination of injected faults and/or input values that causes said determined property to fail.

7. A method according to claim 6, wherein said combination of injected faults and/or input values causing the determined property to fail corresponds to a scenario that can enable the model of the physical system to be corrected to make it more robust.

8. A method according to claim 1, wherein the combination of faults is selected from a predefined set of faults.

9. A method according to claim 1, wherein the determined property expresses a state or a behavior of said physical system.

10. A method according to claim 9, wherein the determined property is a safety property of said physical system.

11. The method of claim 1, wherein the first model of the physical system is an electronic system comprising at least one computer for controlling an engine.

12. 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.

13. A system according to claim 12, wherein the mechanism for injecting faults comprises a fault input interface and fault applier means.

14. A system according to claim 12, wherein the physical system is an electronic system comprising two computers for controlling an airplane engine.

15. The system of claim 12, wherein the first model of the physical system is an electronic system comprising at least one computer for controlling an engine.