4266

The invention is a unique reachability resolution method that has been developed based on the refinement of the hybrid automation such that the reachability is reduced to the reachability in the underlying graph (without the dynamics) whenever the refinement step terminates.  This approach yields a technique that is effective in terms of achieving test coverage and efficient in terms of test generation time.  Software is available for testing.

Simulink/Stateflow is a popular commercial model-based development tool for many industrial applications.  For safety and security concerns, verification and testing must be performed on the Simulink/Stateflow designs and the generated code.  In this design, a novel test generation approach is presented by reduction to reachability in a Hybrid Automation, with its locations representing the computations of the model, and edges representing the computation-succession.  A unique reachability resolution method has been developed based on the refinement of the hybrid automation such that the reachability is reduced to the reachability in the underlying graph (without the dynamics) whenever the refinement step terminates.  This approach yields a technique that is effective in terms of achieving test coverage and efficient in terms of test generation time.

This technology is related to ISURF #3739:  Modeling Approach for Simulink/Stateflow Diagrams to Ease Analysis of Embedded Software

• The problem of eventual executability of a computation path to that of reachability in a discrete-time computation-succession hybrid automation (CS-HA)

• A recursive refinement of CS-HA that preserves reachability to graph connectivity

• An algorithm to obtain a test that eventually executes a reachable computational path.

• Easy integration into Simulink.

• Automatically and efficiently generate test cases for Simulink/Stateflow models with feedback loops

Applications that requires automatic test generation in model-based development using Simulink/Stateflow