Efficient Black-Box Checking with Specification-Guided Abstraction

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.