# US 2014/0195208 A1 · Efficient partition refinement based reachability checking for simulinks/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/0195208 A1
- Document ID: US20140195208A1
- Status: Published application
- Kind: A1
- Application number: 13/737,227
- 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: Srihari Sukumaran; Manoranjan Satpathy
- Web page: https://patentgrep.com/patent/US20140195208A1

## 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 between states in a transition system using simulation modeling. Generating a concrete simulation model. Generating an abstract model having an abstract path that is a sequence of transition steps between a source state and a target state. Validity of the abstract path is checked. Identifying whether the abstract path is invalid in the concrete model. If invalid, then discarding the abstract path and generating a new abstract path. Re-checking a validity of each new abstract path. If abstract path is valid, then determining whether the abstract path is reachable from an initial condition. If reachable, then outputting the reachable transition to the user; otherwise, partitioning the source state into two additional state abstractions. Recomputing a refined abstract model retaining all transition paths except transitions that are determinative as invalid. Rechecking validity of an abstract path associated with the refined abstract model.

## Claims

### Claim 1

A method for verifying reachability of a transition between states with respect to design and simulation modeling, the method comprising the steps of:
generating a concrete simulation model by a processor as a transition system;
generating an abstract model by the processor having an abstract path that is a sequence of transition steps between a source state and a target state, the source state being an inverse of the target state;
checking a validity of the abstract path by the processor utilizing the concrete simulation model;
outputting a result to a user by an output device that identifies whether the abstract path is invalid in the concrete model; if invalid then;
discarding the abstract path;
generating a new abstract path by an output device;
re-checking a validity of each new abstract path by the processor;
if abstract path is valid in the concrete model, then determining whether the abstract path is reachable from an initial condition;
if reachable from the initial condition, then outputting the result to the user identifying the reachable transition between the source state and the target state;
otherwise, partitioning the source state into two additional state abstractions by the processor;
recomputing a refined abstract model by the processor retaining all transition paths except transitions that are determinative as invalid, the refined abstract model including a sequence of non-discarded transition steps;
rechecking validity of an abstract path associated with the refined abstract model using the concrete model; and
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.

### Claim 2 (depends on 1)

The method of claim 1 wherein the source state is initially partitioned as a two state abstraction.

### Claim 3 (depends on 2)

The method of claim 2 wherein initially partitioning the source state is based on a pre-image of a respective transition partitioned two state abstraction.

### Claim 4 (depends on 3)

The method of claim 3 wherein the each of the abstract states partitioned after the source state has a valid outgoing transition step.

### Claim 5 (depends on 1)

The method of claim 1 wherein the step of retaining all transition paths except transitions that are determinative as unreachable is performed without using a solver.

### Claim 6 (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 7 (depends on 1)

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

### Claim 8 (depends on 1)

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

### Claim 9 (depends on 1)

The method of claim 1 wherein a processor is used for determining whether each transition out of the abstract state in the current abstract model will be reachable in and out of the partitioned states of the refined abstract model.

### Claim 10 (depends on 1)

The method of claim 1 wherein a processor is used for determining whether a transition out of the abstract state in the current abstract model is valid in the concrete model.

### Claim 11 (depends on 1)

The method of claim 1 wherein recomputing a refined abstract model further includes discarding transition abstract paths that are determinative as unreachable.