Systematic Testing of Reactive Software with Non-Deterministic Events: A Case Study on LG Electric Oven

Most home appliance devices such as electric ovens are reactive systems which repeat receiving a user input/event through an event handler, updating their internal state based on the input, and generating outputs. A challenge to test a reactive program is to check if the program correctly reacts to various non-deterministic sequence of events because an unexpected sequence of events may make the system fail due to the race conditions between the main loop and asynchronous event handlers. Thus, it is important to systematically generate/test various sequences of events by controlling the order of events and relative timing of event occurrences with respect to the main loop execution. In this paper, we report our industrial experience to solve the aforementioned problem by developing a systematic event generation framework based on concolic testing technique. We have applied the framework to a LG electric oven and detected several critical bugs including one that makes the oven ignore user inputs due to the illegal state transition.