Improving an Industrial Test Generation Tool Using SMT Solver
Hao Ren, Devesh Bhatt, Jan Hvozdovic · Lecture notes in computer science · 2016
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. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.