Efficient Black-Box Checking via Model Checking with Strengthened Specifications

TL;DR

This paper proposes an improved black-box checking method for cyber-physical systems that uses strengthened specifications in model checking to more efficiently identify violations and reduce the need for time-consuming equivalence testing.

Contribution

It introduces a novel approach that enhances black-box checking by employing strengthened specifications in model checking, leading to more efficient violation detection.

Findings

Increased likelihood of finding violation inputs with strengthened specifications

Reduced number of equivalence tests needed

Demonstrated effectiveness on automotive benchmark

Abstract

Black-box checking (BBC)} is a testing method for cyber-physical systems (CPSs) as well as software systems. BBC consists of active automata learning and model checking; a Mealy machine is learned from the system under test (SUT), and the learned Mealy machine is verified against a specification using model checking. When the Mealy machine violates the specification, the model checker returns an input witnessing the specification violation of the Mealy machine. We use it to refine the Mealy machine or conclude that the SUT violates the specification. Otherwise, we conduct equivalence testing to find an input witnessing the difference between the Mealy machine and the SUT. In the BBC for CPSs, equivalence testing tends to be time-consuming due to the time for the system execution. In this paper, we enhance the BBC utilizing model checking with strengthened specifications. By model checking with a strengthened specification, we have more chance to obtain an input witnessing the specification violation than model checking with the original specification. The refinement of the Mealy machine with such an input tends to reduce the number of equivalence testing, which improves the efficiency. We conducted experiments with an automotive benchmark. Our experiment results demonstrate the merit of our method.