Efficient Black-Box Checking via Model Checking with Strengthened Specifications
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.
Thu 12 MayDisplayed time zone: Osaka, Sapporo, Tokyo change
13:00 - 16:00 | |||
13:00 45mTalk | Efficient Black-Box Checking via Model Checking with Strengthened Specifications AiDL 2022 Junya Shijubo Kyoto University | ||
13:45 45mTalk | Weakest Preconditions in Fibrations AiDL 2022 Shin-ya Katsumata National Institute of Informatics | ||
14:30 90mMeeting | Discussion (3) AiDL 2022 |