Compositional Test Generation of Industrial Synchronous Systems
This addresses the critical problem of test generation for developers of safe embedded systems, though it is incremental as it builds on existing verification techniques.
The paper tackled the complexity of test generation for industrial synchronous systems by proposing a compositional method that treats test cases as counterexamples in safety verification, successfully generating test cases for four industrial examples where existing tools failed.
Synchronous systems provide a basic model of embedded systems and industrial systems are modeled as Simulink diagrams and/or Lustre programs. Although the test generation problem is critical in the development of safe systems, it often fails because of the spatial and temporal complexity of the system descriptions. This paper presents a compositional test generation method to address the complexity issue. We regard a test case as a counterexample in safety verification, and represent a test generation process as a deductive proof tree built with dedicated inference rules; we conduct both spatial- and temporal-compositional reasoning along with a modular system structure. A proof tree is generated using our semi-automated scheme involving manual effort on contract generation and automatic processes for counterexample search with SMT solvers. As case studies, the proposed method is applied to four industrial examples involving such features as enabled/triggered subsystems, multiple execution rates, filter components, and nested counters. In the experiments, we successfully generated test cases for target systems that were difficult to deal with using the existing tools.