Improving an Industrial Test Generation Tool Using SMT Solver

As the industry practices engage model-based design increasingly, model-based verification and testing [1] techniques emerge to keep up with the trends. In avionics area, comprehensive testing methods and tools are required to assure that safety-critical systems like flight controls are certified to the guidelines established by standard processes such as the DO-178C [2].

At Honeywell, researchers have developed the Honeywell Integrated Lifecycle Tools & Environment (HiLiTE) suite of tools for the automated verification of avionics applications developed using MATLAB Simulink/Stateflow. HiLiTE performs automatic test generation [3] on Simulink models based upon the low-level requirements (LLRs) expressed by the model elements. The tests are then applied to the executable object code generated from the model to verify that the code complies with the LLRs in the design model. HiLiTE has been qualified as a DO-178C verification tool and deployed in several avionics product certifications to deliver significant cost savings in the verification effort.

This paper presents an SMT solving technique to extend the earlier heuristics-based test case generation approaches implemented in HiLiTE, providing improved performance on models with complex constraints or non-linear arithmetic computations. SMT solving is the decision procedure of determining whether a formula in first-order-logic is satisfiable and finding a concrete solution if it is. SMT Solvers, such as Z3 [4], Yices [5], etc., have rapidly matured over the last 5 years and have been used in various areas including automated test case generation [6, 7]. In our SMT solving based approach, each LLR equivalence class for a block type is represented by a set of constraints, applied on block-level input(s) and expected output. Meanwhile, test space is also constrained by the subgraph environment that the block under test (BUT) is embedded in. The collection of constraints can be formulated as an SMT problem and expressed in a standard format by HiLiTE in an automatic fashion. SMT solver is then called to generate the satisfiable solution once for all ports in the related subgraph. The solution is merged back to the entire graph for a complete model-level input-to-output test case. With the integration of heuristics and SMT solving techniques, HiLiTE has been successfully used to generate requirement-based test cases for a great range of large-scale complex constrained avionics models.

Section 2 describes the HiLiTE normal test case generation approach and the need for improvements. Section 3 describes the formalized language of equivalence classes of block’s behaviors and SMT solving based test case generation approach. Finally, the conclusion and future work are discussed in Sect. 4.

HiLiTE generates specific tests at the model level to exercise the equivalence classes of the behavior of each block embedded in the model. In the original HiLiTE tool, each equivalence class of a block’s behavior is represented by a set of test case templates, each of which uses heuristics to select a specific combination of values for the block under test (BUT) input(s) and output that satisfy this equivalence class. Backward and forward propagation search through the computations of other blocks in the model generates a test vector in terms of model inputs and outputs to ensure controllability of the BUT inputs and observability of the expected BUT output. Figure 1 shows a Simulink model extracted from a complex industrial model to illustrate this.

When the product block is the BUT, the test case template (Fig. 2) assigns the two inputs with non-zero values 2 and 4 respectively. After the backward and forward propagation search, the generated test vectors are given in Fig. 2 where blue column heading denotes model input and green denotes model output.

When the switch block is the BUT, the equivalence class requires different values at its data inputs (FalseIn, TrueIn) to verify unique impact of an input on the block’s output. One test case template assigns 44 to FalseIn and 46 to TrueIn, but this leads to a conflict at the model input AdjustPct after backward computation through the two look-up tables since their data points are in the same range. HiLiTE then further tries several alternative templates based on heuristics, yet all result in search failure. The root cause is that HiLiTE templates heuristics in the equivalence class domain prematurely pick block’s local input values, while this problem involves taking into account constraints imposed by the look-up table blocks driven by the same input AdjustPct.

Test generation difficulties such as those noted above can be addressed by an approach that solves computational constraints of the upstream subgraph of BUT in conjunction with the constraints on BUT inputs imposed by the behavior equivalence class. SMT can be thought of the constraint satisfaction problem expressed in Boolean formulas, linear/nonlinear arithmetic in integer/real domain, bit-vectors and so on. In HiLiTE, we added SMT solving based approach that embodies formulating test case generation constraints from both equivalence classes, constraints related to upstream source ports and the subgraph computations upstream of the BUT into an SMT problem. Therefore, constraints can be solved together to find a satisfying solution which excludes any conflicts.

We extended the HiLiTE test generation capability with an SMT solving based approach for solving certain complex constrained problems. The improved tool combines HiLiTE normal search method and SMT solving, and has been successfully applied on many large-scale industrial models. HiLiTE is also being extended to derive invariant bounds on the number of time steps (e.g., for a timer) that will help bound the array size. We are also applying SMT solving to support such invariant generation, in which each condition-guarded path that captures a certain pattern of model behavior can be validated by SMT solving.