Systematic Evaluation of Black-Box Checking for Fast Bug Detection
Bram Pellen, Mar\'ia Bel\'en Rodr\'iguez, Frits Vaandrager, Petra van den Bos

TL;DR
This paper systematically evaluates black-box checking (BBC) for bug detection, demonstrating its efficiency and effectiveness in quickly identifying violations in real-world protocol models and controllers, outperforming traditional methods.
Contribution
First comprehensive assessment of BBC's ability to detect bugs rapidly across diverse benchmarks, highlighting its advantages over existing model-based testing approaches.
Findings
BBC detects violations with only 3.4% of queries compared to full model checking.
BBC finds 94% of violations in challenging industrial benchmarks.
BBC outperforms existing model-based testing algorithms in deep bug detection.
Abstract
Combinations of active automata learning, model-based testing and model checking have been successfully used in numerous applications, e.g., for spotting bugs in implementations of major network protocols and to support refactoring of embedded controllers. However, in the large majority of these applications, model checking is only used at the very end, when no counterexample can be found anymore for the latest hypothesis model. This contrasts with the original proposal of black-box checking (BBC) by Peled, Vardi & Yannakakis, which applies model checking for all hypotheses, also the intermediate ones. In this article, we present the first systematic evaluation of the ability of BBC to find bugs quickly, based on 77 benchmarks models from real protocol implementations and controllers for which specifications of safety properties are available. Our main finding are: (a) In cases where…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Machine Learning and Algorithms · Software Testing and Debugging Techniques
