Granted Patent B2

US 8,275,729 · App. 11/749,768 · Granted Sep 25, 2012

Assignee: GM Global Technology Operations LLC

Abstract

Claims (56)

1. Method for verifying linear hybrid automaton, the method comprising:

using a reachability analysis of a linear transition system (LTS) to verify a linear hybrid automata (LHA) system;

generating initial abstract model based on an original Linear-Time Temporal Logic (LTL) specification;

validating a counterexample using an approach of linear constraints satisfaction;

identifying a fragment in the counterexample by iteratively applying the approach of linear constraints satisfaction; and

refining the original LTL specification based on the fragment derived.

2. The method of claim 1 , wherein generating an initial abstract model comprises:

transferring the LHA into the LTS, wherein the LTS is a discrete transition graph in combination with a set of real variables that consists of discrete dynamics that are modeled by discrete transitions, wherein each discrete transition has a linear transition relation function that relates the real variables before and after each discrete transition, wherein the abstract model includes the LTS discrete transition graph and does not include representations of reachable state sets.

3. The method of claim 2 , further comprising:

checking the abstract model for reachability of a set of bad locations;

determining that the set of bad locations is not reachable in the LTS if the abstract model passes the abstract model checking; and

generating a counterexample if the abstract model does not pass the model checking.

4. The method of claim 3 , further comprising

terminating the method for verifying linear hybrid automaton if the abstract model satisfies the LTL specification.

5. The method of claim 3 , further comprising:

checking the feasibility of the counterexample in the LTS to determine whether a corresponding run exists in the LTS for the counterexample.

6. The method of claim 5 , further comprising:

generating a linear constraint satisfaction problem for checking if a corresponding run exists in the LTS;

solving the linear constraint satisfaction problem to determine if a run of bad location sets exists in the LTS for the counterexample; and

using the run as a concrete counterexample if the bad location sets is reachable in the run of the LTS, wherein the run of bad location sets is reachable in the LTS if the LTL specification is not satisfied.

7. The method of claim 6 , further comprising:

identifying a fragment in an invalid counterexample that is infeasible in the LTS; and

refining the system specification based on the invalid counterexample fragment.

8. The method of claim 3 , further comprising:

using an approach of linear constraints to validate the counterexample if the LTL specification is not satisfied by the abstract model;

determining whether the counterexample is feasible; and

terminating the method for verifying linear hybrid automaton if the counterexample is feasible in the LTS.

9. The method of claim 1 , wherein identifying a fragment in the counterexample by iteratively applying the approach of linear constraints satisfaction comprises:

dividing the identified fragment into a first and a second sub fragment; and

determining if both the first and second sub fragments are valid.

10. The method of claim 9 , further comprising:

randomly picking an invalid sub fragment from one of the first and second sub fragments; and

determining if the randomly picked invalid sub fragment has a length equal to one.

11. The method of claim 9 , further comprising:

identifying a fragment in an invalid counterexample that is infeasible in the LTS repeatedly until the first and the second sub fragments are both valid or until the length of an invalid fragment equals one.

12. The method of claim 1 , further comprising:

refining the specification to include the initial specification and the specification based on the fragment identified such that each run in the abstract model either does not contain any bad state location or contains the fragment before reaching a bad location.

13. The method of claim 12 , wherein refining the specification further comprises:

identifying a minimal conflict constraint set for the counterexample fragment identified.

14. The method of claim 13 , further comprising:

using incremental linear constraint solving algorithms to identify the minimal conflict constraint set.

15. The method of claim 14 , further comprising:

deriving a set of fragments based on the minimal conflict constraint set and a concurrency of concurrent systems.

16. The method of claim 15 , further comprising:

using a LTL formula to encode a plurality of system traces that contain a fragment from the set of fragments before reaching any bad locations.

17. The method of claim 15 , further comprising:

refining the original LTL specification by adding the LTL formula derived from the set of fragmented such that either the original LTL specification is satisfied or the added LTL specification is satisfied.

18. The method of claim 1 , further comprising:

using the reachability analysis to verify an embedded control system.

19. The method of claim 1 , further comprising:

implementing the reachability analysis to verify that the linear hybrid automata system on a software tool that is executed on a computer system having associated microprocessor means including an arithmetic processor and associated memory means.

20. Method for verifying linear hybrid automaton, the method comprising:

generating an initial abstract model based on an original Linear-Time Temporal Logic (LTL) specification;

validating a counterexample using an approach of linear constraints satisfaction;

identifying a fragment in the counterexample by iteratively applying the approach of linear constraints satisfaction in a predefined number of times; and

refining the original LTL specification based on the fragment derived.

Assignments (11)

Continuity (2)