3739

Iowa State University researchers have developed a modeling approach for Simulink diagrams that can be used for further analysis such as test generation and formal verification.

This modeling approach is available for testing

Simulink is a commercial tool for graphical representation and simulation of dynamic systems, and Simulink/Stateflow (S/S) diagrams can be used to capture time or event-driven dynamics.  Simulation of S/S diagrams can be use to generate sample runs for validation. Further validation can be performed through testing, verification and monitoring, with automated testing, verification and monitoring desirable.  However, current approaches for modeling S/S diagrams in a format amenable to automatic test generation, verification and monitoring are inadequate.  To overcome this limitation, ISU researchers have developed a modeling approach for an industry-level useful fragment of Simulink/Stateflow diagrams using input/output extended finite automata (I/O-EFA), which is a formal model amenable for analysis.  The input-output behavior of an I/O-EFA model, as defined in terms of a step-trajectory, preserves the input-output behavior of the corresponding Simulink/Stateflow diagram at each sample time.  This approach is recursive and modular that models atomic blocks and recursively and modularly combines such blocks for forming models of more complex Simulink/Stateflow diagrams from the simpler ones.  The modeling approach has utility for automated test generation, verification or monitoring for fault-detection of embedded software developed using Simulink/Stateflow diagrams, or other similar simulation tools such as LabView.

This technology is related to ISURF #4266:  Reduction of Automated Test Generation for Simulink/Stateflow to Reachability and its Novel Resolution

• Efficient (modeling is recursive and modular)

• Effective  (amenable to automated test generation for comprehensive coverage such as MCDC or comprehensive verification, monitoring, and fault-detection)

• Versatile (can be applied to industry-level useful fragment of Simulink/Stateflow)

• Precise (precisely preserves the discrete-time semantics)

Conference Proceedings: "Modeling Simulink Diagrams using Input/Output Extended Finite Automata", Changyan Zho and Ratnesh Kumar, 2009, 6th International Workshop on Software Cybernetics, Seattle, WA.