Exploring Design Verifier - 05

Exploring Stateflow Mutation and Simulink Design Verifier

In this submission an autopilot Stateflow model is mutated using a Matlab script. Mutation of a Stateflow model means injecting a deliberate error into a state transition. Each mutant file has only one error. Simulink Design Verifier is then used to find the mutants. If an assertion fails it means that the mutant is killed. The script is able to generate mutants for this particular Stateflow model. With minor changes it should be able to mutate any Stateflow. Another batch script runs all the mutants in a loop and reports the results in a log file. The PDF file has a brief explanation of the work done. The intent of this exercise is to ascertain the SLDV performance on a complex aerospace problem. Earlier submission had a Simulink model and a M file function model for the same autopilot mode transition. The M File is modified here to write a sldv command for every requirement. This is then used to generate requirement based tests for the Stateflow model by falsifying the assertion.