Systematic Testing of Reactive Software - A Case Study on LG Electric Oven
Overview of a case study conducted on LG Electric Oven using systematic testing of reactive software with non-deterministic events. The study focused on detecting concurrency bugs in the software controller of the oven through an automated testing framework that generates event timing sequences. It emphasized the importance of testing reactive programs in controller devices to identify and address corner-case bugs that may be hard to detect. The research highlighted the challenges posed by the non-deterministic nature of event ordering and timing in reactive software.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven Yongbase Park, Shin Hong, Moonzoo Kim, Dongju Lee, Junhee Cho Software Testing and Verification Group (SWTV) http://swtv.kaist.ac.kr S. Hong @ KAIST / 18
Safety Problems due to Poor Quality of SW jupiter 1st test flight.jpg Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 2 S. Hong @ KAIST / 18 2024-10-02
Strong IT Industry in South Korea Time-to- Market? SW Quality? Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 3 S. Hong @ KAIST / 18 2024-10-02
Overview Reactive programs can have subtle concurrency errors as their behaviors depend on timing of input events We developed an automated testing framework that generates event timing/sequences systematically to detect concurrency bugs We found 3 new concurrency bugs in the controller S/W of the LG electric oven product Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 4 S. Hong @ KAIST / 18 2024-10-02
Reactive Programs in Controller Devices A reactive program repeats: (1) receiving an input (2) updating the internal state for the new input (3) generating output w.r.t the new state A reactive program utilizes non-deterministic interrupt handlers to receive a given input event immediately Embedded software on 8-bit MCU does not use standard synchronization since OS is not supported Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 5 S. Hong @ KAIST / 18 2024-10-02
Hard to Detect Corner-Case Bugs in Reactive Software Reactive software may have various execution scenarios because of various event ordering and event timing A corner-case bug only occurs on specific event ordering and event timing Reactive software may suffer from corner-case bugs, which are hard to detect Scenario #1 Scenario #N Buggy Scenario int cnt=1; void main() { while(1) { if(cnt>0) { int x=10/cnt; print(x); } cnt++; }} void handler() { cnt=0; } 1 2 3 4 5 6 7 8 9 11: cnt=0 4: if(cnt>0) 4: if(cnt>0) 11: cnt=0 4: if(cnt>0) 5: x=10/cnt 8: cnt++ 6: print(x) 5: x=10/cnt Error! 8: cnt++ 11: cnt=0 10 11 Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 6 S. Hong @ KAIST / 18 2024-10-02
Challenges in Testing Reactive Programs Tests should cover all event sequence, together with all timing of events for each sequence Infeasible for human testers No proper automated testing techniques Random noise injection technique is not effective and not efficient for finding concurrency bugs Model checkers for multithreaded programs are not scalable to verify real-world controller software Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 7 S. Hong @ KAIST / 18 2024-10-02
Systematic Event Generation Framework 1. Instrument a target reactive program to invoke an event handler in a middle of the main loop depending on symbolic values 2. Use conclic testing to systematically generate symbolic values to cover all event scenarios Program inputs Concolic testing Target program Code transform. transform. Transformed program Code Event scenarios CREST-BV Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 8 8 S. Hong @ KAIST / 18 2024-10-02
Code Transformation for Concolic Testing Insert a probe for every statement the main loop A probe invokes an event handler if its activation condition is satisfied in an execution Define the activation condition of each probe at each main loop iteration as symbolic values EventScenario main() { symEventScenario(); while (1) { if(act(2)) evHdr(); int t = 0 ; if(act(3)) evHdr(); data = 10 ; if(act(4)) evHdr(); f(data) ; } } main() { while (1) { int t = 0 ; data = 10 ; f(data) ; } } Active probe Iter 1 2 3 4 5 1st 2 0 2nd 3 0 3rd 2 4 evHdr(){ } 11 evHdr(){ } Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 9 S. Hong @ KAIST / 18 2024-10-02
Contributions Reported the real-world challenges to test reactive programs with non-deterministic events Developed a systematic event generation (SEG) framework to generate various event scenarios Demonstrated the effectiveness of the SEG framework by detecting 3 new bugs from LG electric oven S/W Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 10 S. Hong @ KAIST / 18 2024-10-02
Project Background Target: embedded S/W on a high-end electric oven 19,650 lines of C code (180 files, 658 functions) The project takes 5 months in 2014 Team 1 research engineer in LG CTO 1 field developer in LGE H/A 2 graduate students + 1 professor in KAIST The source code, test cases, state-transition diagram, and emulator of the target system is given to the KAIST members. Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 11 S. Hong @ KAIST / 18 2024-10-02
Oven Controller Software Key/door Event Handler LED Key input Handler Shared memory Shared memory Main Loop LED LED output command Shared memory Input buffer CircularQueue Door input Cooking command Timed Event Handler Cook Command Handler Cooking device control output Timer Test drivers Test targets Test oracle Unit Testing of CircularQueue 145 LOC Invariants of Queue data structure Integration testing 12,691 LOC System state transitions diagram spec Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 12 S. Hong @ KAIST / 18 2024-10-02
Unit Testing Overview CircularQueue enqueue() inserts an element if the queue is not full dequeue() returns and removes the oldest member in the queue if the queue is not empty CircularQueue Test scenario the main loop performs dequeue(), and the event handlers perform enqueue() concurrently Key/door Event Handler dequeue() enqueue() Shared memory Main Loop Key input Shared memory Input buffer Two multi-variable atomicity violations are detected Overwriting bug: unintentionally overwrite the oldest value with a new value Inconsistency bug: unintentionally remove all values Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 13 S. Hong @ KAIST / 18 2024-10-02
Inconsistency Bug CircularQueue status Main loop void* dequeue() { void* r = NULL; if (!isEmpty()) { r = head; head=getNextIdx( ); isFull = FALSE;} return r;} 7 1 2 3 4 5 6 Arr 1 isFull ==false 2 - tail head Arr 1 isFull ==false 2 - event tail head enqueue(3) event Arr 4 isFull ==true enqueue(4) 2 3 head tail Arr isFull ==false isEmpty()==true as isFull==false && head==tail 4 2 3 tail head Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 14 S. Hong @ KAIST / 18 2024-10-02
Testing Performance Average time to detect fault Technique Fault detection SEG 100% 15 sec 0-500 ?sec 0-1000 ?sec 20% 1653 sec Random 23% 1578 sec 0-1500 ?sec 0% - SEG is more effective to find the inconsistency bug than then random noise injection-based testing techniques Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 15 S. Hong @ KAIST / 18 2024-10-02
Integration Testing We tested all code of the main loop and the key event handlers SEG found illegal transition bug An error occurs when the oven control software retrieves multiple input events from the input buffer Main loop Main loop dequeue 2 dequeue auto-cook auto-cook Input buffer function-R dequeue function-R Input buffer Input buffer Error Success Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven S. Hong @ KAIST / 18 2024-10-02 16
Lessons Learned on Effective Technology Transfer The developers were happy to adopt the SEG framework because Our group has 10 years experience in industrial collaboration with Samsung, LG, and Hyundai The developers are well-trained about the technique (i.e., concolic testing) so that they can adapt the tool for their needs In 2012, Prof. Kim made 8 weeks of seminars on automated testing techniques to the field engineers of LGE In 2013, a pilot study was made to apply concolic testing techniques to LGE software In 2015, a new target domain (i.e., washing machines) is being explored and plan to test robot vacuum cleaners next Use success stories w/ other industries as a reference Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 17 S. Hong @ KAIST / 18 2024-10-02
Conclusion and Future Work SEG effectively detects corner-case concurrency bugs in real-world embedded software SEG generates event timing and sequences systematically SEG found 3 new bugs and improved the target S/W quality SEG found similar concurrency bugs from clock- source device drivers in Linux 3.19 We had reported 3 new bugs, and the developers made patches for these bugs Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 18 S. Hong @ KAIST / 18 2024-10-02
Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven Yongbase Park, Shin Hong, Moonzoo Kim, Dongju Lee, Junhee Cho KAIST LG Electronics S. Hong @ KAIST / 18
Reactive Program The main loop repeats: (1) receive an input from an event handler (2) update the internal state w.r.t the new input (3) generate output w.r.t the new state If an input event is given, the main loop is suspended immediately and the event handler is executed instead MCU User CPU User CPU User evHdr1(){ e11; e1N ; } evHdr2(){ e21; e2K; } main(){ while(1){ m1; mL ; } } m1 m1; mL; e1 ; eN; e1 ; eN; e1 ; eN; m1; mL; m2; mL; 20 20 Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven S. Hong @ KAIST / 18 2024-10-02
Challenges in Reactive Software Testing Reactive software may suffer from concurrency errors, which are hard to detect In manual testing Human testers cannot precisely control all possible timing of events Human testers may not design complex event scenarios as test cases In automated testing by conventional techniques Conventional concolic testing does not generate various order/timing of events Model checking technique [Chandra 02] [Fidge 05] [Holzmann 99] is not effective for checking reactive software in industry due to high cost of abstract model creation and state explosion problems Noise injection random testing [Lei 05] [Stoller 02] may not find corner-case bugs with low possibility of detection Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 21 S. Hong @ KAIST / 18 2024-10-02
Model Checking Model checking techniques exhaustively and automatically check whether a given model meets a given specification Previous works created models of reactive software with human efforts [Fidge, 05] and [Chandra, 02] create the target model manually [Holzmann, 99] semi-automatically generates a model using a user-giv en translation table Limitations Developers in industry cannot afford time to create abstract models for reactive software due to hard time-to-market pressure Model checking techniques may not generate results within limited time and memory space due to state explosion problem The number of states of given model increases exponentially with the number of events Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 22 S. Hong @ KAIST / 18 2024-10-02
Concolic Testing Concolic (CONCrete + symbOLIC) testing (dynamic symbolic execution) aims to explore all paths of the given program 1. run a given program with concrete inputs 2. create a symbolic path constraint from the concrete execution 3. negate a branch of the symbolic path constraint 4. generate a new test input that satisfies the negated constraint void main() { if(evId==0)handler(); stmt1; if(evId==1)handler(); stmt2; } No. evId 1 0 1 0 1 0 1 0 1 2 3 4 5 6 No. No. No. main() main() main() main() F F F F evId==0 evId==0 evId==0 evId==0 T T T T handler() handler() handler() handler() stmt1 stmt1 stmt1 stmt1 Sym. path evId==0&&evId!=1 evId==0&&evId!=1 evId==0&&evId!=1 evId==0&&evId!=1 Sym. path Sym. path Sym. path constraint Negated path Negated path Negated path constraint Negated path evId==0&&evId==1 evId==0&&evId==1 evId==0&&evId==1 evId==0&&evId==1 evId evId evId evId==1 evId==1 evId==1 evId==1 T T T T F F F F handler() handler() handler() handler() evId!=0 evId!=0 evId!=0 stmt2 stmt2 stmt2 stmt2 2 3 1 1 evId!=0&&evId==1 evId!=0&&evId==1 evId!=0&&evId!=1 2 return return return return Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 2 S. Hong @ KAIST evId!=0&&evId!=1 23 / 18 2024-10-02 evId!=0&&evId!=1
Noise Injection Random Testing To generate divers execution scenario, [Lei, 05] presents a t echnique that inserts random noise before message generation code in a message-passing program Limitation: noise injection random testing may not find corner-case bugs with low possibility of detection 1 handler() call between miand mi+1 2 handler() calls between miand mi+1 void main() { while( ) { m1; m2; mL; } } void handler() { } void evGeneration() { sleep(rand());genEv(); sleep(rand());genEv(); } 2024-10-02 1 2 3 4 5 6 7 8 9 CPU CPU CPU m1; mi; m1; mi; handler() m1; mi; handler() handler() mi+1; mL; handler() handler() 10 11 12 mi+1; mL; mi+1; mL; Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven handler() 24 S. Hong @ KAIST / 18
Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven Symbolic Variable & Probe Setup A function init() declares each e lement of evLoc as a symbolic vari able init() is called before execution of m ain loop isInHandler is a flag to prevent nested event handler executions int evLoc[MAX_IT][MAX_EV]; void init() { for(i=0;i<MAX_IT;i++) for(j=0;j<MAX_EV;j++) CREST_int(evLoc[i][j]); } void probe(int locId) { static int isInHandler=FALSE; if(!isInHandler) { for(j=0;j<MAX_EV;j++) { if(evLoc[iter][j]==locId){ isInHandler = TRUE; eventHandler(); evLoc[iter][j] = DONE; isInHandler = FALSE; } } } } 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 In the case study subject, nested event handler executions are not allowed An event handler may call probe() be cause of functions that both main loop and the event handler call If evLoc[iter] contains locId, an event handler is called 25 S. Hong @ KAIST / 18 2024-10-02
Target Electric Oven 8-bit MCU LED display Key interface Steam outlet Charcoal heater Door Roast heater Microwave emitter LED display Multi- clean button Steam button Adjust dial Select button Cancel button Feature dial Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 26 S. Hong @ KAIST / 18 2024-10-02
Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven Overwriting Bug CQ status Main loop execution qArray queueFull ==true 1 2 3 1:dequeue() headIdx tailIdx qArray queueFull ==false 6:queueFull =false; event 1 2 3 headIdx tailIdx result enqueue(4) qArray queueFull ==true 4 2 3 8:return result; headIdx tailIdx result 27 S. Hong @ KAIST / 18 2024-10-02
Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG El ectric Oven Illegal Transition Bug The illegal transition occurs when the main loop handles multiple key events at the same time - The oven freezes due to the illegal state auto-cook function-R control menu, manual-cook Initial state 5 sec defrost control init, default menu, default menu, menu, clean-defrost cook-option auto-cook auto-cook & function-R enter enter function-R States in the cooking mode cooking, simple-cook cooking, default cooking, preheating cooking, manual-cook complete Legend complete curMode, curView finish, default event door open complete Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 28 S. Hong @ KAIST / 18 2024-10-02
Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven Bug Detection Time of SEG The following table shows the error detection results of the illegal transiti on bug of random search strategy DFS search strategy failed to detect the bug because of large search space SVA detects the illegal transition bug faster than the other 2 strategy beca use SVA reduce search space by inserting less probes SVA achieves higher coverage than the others because SVA negates more i nput-related branches than the other technique Branch Coverag e Technique Detection Time # of executions STMT BB SVA STMT BB SVA STMT BB SVA 195.10 172.63 113.63 208.60 249.43 150.47 280.03 249.63 197.93 3991.40 3800.33 2932.10 2920.60 3845.10 2858.57 3210.60 50.2% 50.0% 50.9% 51.8% 51.7% 52.1% 52.6% 52.8% 53.4% MAX_EVENT=2 MAX_EVENT=3 SEG MAX_EVENT=4 S. Hong @ KAIST 3307.43 2594.03 29 / 18 2024-10-02
Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven State Transition Example 30 S. Hong @ KAIST / 18 2024-10-02
Unit Testing Overview Test scenario: the main loop performs dequeue(), and event handlers can perform enqueue() concurrently Bug detection Overwriting bug: unintentionally overwrite the oldest value in the que ue with a new value Inconsistency bug: unintentionally remove all values in the queue CircularQueue status Main loop execution 5:headIdx= getNextIdx( ) void* dequeue() { void* result = NULL; if (!isEmpty()) { result = headIdx; headIdx=getNextIdx( ); queueFull = FALSE; } return result; } 2024-10-02 qArray 1 1 2 3 4 5 6 7 8 9 queueFull ==false 2 - event tailIdx headIdx enqueue(3) qArray queueFull ==false 1 2 3 6:queueFull S. Hong @ KAIST =false Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 31 / 18 tailIdx headIdx
Result with SEG Framework Fully automated testing technique The SEG approach requires than model checking and ad- hoc random testing Effective in fault finding Control event timing in a fine-grained manner Generate all event scenarios systematically Found 3 new bugs in LG electric-oven S/W and improved software quality 2 bugs in unit-level testing of CircularQueue 1 bugs in integration-level testing of the main loop and the key event handlers Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven 32 S. Hong @ KAIST / 18 2024-10-02
