2021/12/10 by Daisuke Ishii, Takashi Tomita, Ishii, Daisuke +5
Computer Science · Engineering · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Safety Systems Engineering in Autonomy #Software Engineering (cs.SE) #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.2112.05411
openalex publication_date 2021/12/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.