FLOPS 2022
Tue 10 - Thu 12 May 2022 Online
Thu 12 May 2022 13:00 - 13:45 at 大講演室 - Day 3

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 May

Displayed time zone: Osaka, Sapporo, Tokyo change

13:00 - 16:00
13:00
45m
Talk
Efficient Black-Box Checking via Model Checking with Strengthened Specifications
AiDL 2022
Junya Shijubo Kyoto University
13:45
45m
Talk
Weakest Preconditions in Fibrations
AiDL 2022
Shin-ya Katsumata National Institute of Informatics
14:30
90m
Meeting
Discussion (3)
AiDL 2022