Compositional Test Generation of Industrial Synchronous Systems

TL;DR

This paper introduces a compositional test generation approach for industrial synchronous systems, effectively handling complexity through modular reasoning and SMT solvers, demonstrated on real-world case studies.

Contribution

It presents a novel compositional method for test generation using deductive proof trees and SMT solvers, improving scalability for complex industrial systems.

Findings

Successfully generated test cases for complex systems

Handled features like triggered subsystems and nested counters

Outperformed existing tools in challenging scenarios

Abstract

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.