Improving an Industrial Test Generation Tool Using SMT Solver

We present an SMT solving based test generation approach for MATLAB Simulink designs, implemented in the HiLiTE tool developed by Honeywell for verification of avionic systems. The test requirements for a Simulink model are represented by a set of behavioral equivalence classes for each block in the model, in terms of its input(s) and output. A unique feature of our approach is that the equivalence class definitions, as well as the upstream subgraph of a block under test, are translated as constraints into SMT expressions. An SMT solver is called at the back-end of HiLiTE to find a satisfiable solution that is further augmented into an end-to-end test case at the model level.