# US 2014/0195209 A1 · Counter-Example Guided Abstraction Refinement Based Test Case Generation From Simulink/Stateflow Models

> Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt

- Number: US 2014/0195209 A1
- Document ID: US20140195209A1
- Status: Published application
- Kind: A1
- Application number: 13/737,237
- Filed: 2013-01-09
- Published: 2014-07-10
- Earliest claimed: 2013-01-09
- Assignees: GM Global Technology Operations LLC
- Applicants: GM Global Technology Operations LLC
- Inventors: Manoranjan Satpathy; Srihari Sukumaran; Ambar A. Gadkari
- Web page: https://patentgrep.com/patent/US20140195209A1

## CPC

- G06F 30/20: Design optimisation, verification or simulation (optimisation, verification or simulation of circuit designs G06F30/30)
- G06F 30/3323: using formal methods, e.g. equivalence checking or property checking
- G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N)

## Abstract

A method for verifying reachability of a transition path between states with respect to Simulink/Stateflow models; (a) a concrete simulation model is generated and an abstract model is generated; (c) an abstract path is generated that is a sequence of transition steps from a start state to a target state; (d) a validity of the abstract path is checked utilizing the concrete simulation model; (e) a result is output to a user that identifies the abstract path as a reachable result; (f) partitioning a respective state of the transition step that was invalid in the abstract path; (g) recomputing a next abstract model based on partitioned start state; (h) generating an next abstract path; (i) determining whether the next abstract path is valid; (j) outputting a result to the user that identifies whether the recomputed abstract path is a valid result; otherwise proceeding to step (f).

## Claims

### Claim 1

A method for verifying reachability of a transition path between states with respect to Simulink/Stateflow® models, the method comprising the steps of:
(a) generating a concrete simulation model as a transition system by a processor;
(b) generating an abstract model by the processor;
(c) generating an abstract path by the processor that is a sequence of transition steps from a start state to a target state;
(d) checking a validity of the abstract path by the processor utilizing the concrete simulation model;
(e) outputting a result to a user by an output device that identifies the abstract path as a reachable result; otherwise proceeding to step (f);
(f) partitioning a respective state of the transition step that was invalid in the abstract path by the processor;
(g) recomputing a next abstract model by the processor based on partitioned start state in step (f);
(h) generating an next abstract path by the processor;
(i) determining whether the next abstract path is valid in the concrete model by the processor;
(j) outputting a result to the user by the output device that identifies whether the recomputed abstract path is a valid result for testing the concrete model in a vehicle system; otherwise proceeding to step (f).

### Claim 2 (depends on 1)

The method of claim 1 wherein the start state is a current source state of a current abstract model.

### Claim 3 (depends on 2)

The method of claim 2 wherein only the abstract paths having a length less than a threshold are generated to check the validity.

### Claim 4 (depends on 2)

The method of claim 2 wherein all paths are generated to check validity between the source state and the target state.

### Claim 5 (depends on 4)

The method of claim 4 wherein all paths generated are acyclic paths.

### Claim 6 (depends on 1)

The method of claim 1 wherein the simulation model is a SL/SF model.

### Claim 7 (depends on 1)

The method of claim 1 wherein partitioning a respective state is based on a pre-image of the respective state with respect to the transition step.

### Claim 8 (depends on 1)

The method of claim 1 wherein a set of abstract states in an abstract model is a partition of concrete state in the concrete simulation model.

### Claim 9 (depends on 1)

The method of claim 1 wherein the concrete model and transition paths are tested in a vehicle wiring harness for determining validity of input and output responses.

### Claim 10 (depends on 1)

The method of claim 1 wherein the concrete model and transition paths are implemented in a vehicle.

### Claim 11 (depends on 1)

The method of claim 1 wherein step (g) includes a processor determining whether each transition out of the abstract state in the current abstract model will be feasible in and out of the partitioned states of the next abstract model.

### Claim 12 (depends on 11)

The method of claim 11 wherein the processor is a solver.

### Claim 13 (depends on 12)

The method of claim 12 wherein the solver is a Satisfiably Modulo Theory solver.