Efficient Black-Box Checking with Specification-Guided Abstraction

doi:10.1145/3762659

Return

Efficient Black-Box Checking with Specification-Guided Abstraction

2025-09-01

DOI：10.1145/3762659

Save

View PDF

Abstract

En 中文

Cyber-physical systems (CPSs) often contain components whose internal design is unknown, making their verification challenging. Although black-box checking (BBC)-an automated black-box testing method that combines automata learning and model checking-can detect unsafe behaviors without requiring a complete model, it becomes computationally expensive for large or infinite-state systems. To address this problem, we propose a specification-guided abstraction that identifies and merges states in the system's state space if they are equivalent under the verified specifications. Building on this abstraction, we develop an algorithm that directly learns the resulting abstract Mealy machine, thereby bypassing the need to learn the full system behavior first. We then integrate the new learning procedure with model checking to obtain an enhanced BBC framework that efficiently handles large or infinite-state systems, particularly when verifying multiple properties. Our empirical evaluation demonstrates that specification-guided abstraction improves detection and efficiency in uncovering unsafe behaviors in CPSs.

Keywords:

Testing

linear temporal logic

automata learning

model checking

AI Summary

Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.