Modeling and testing embedded system by model checking

Software testing is the key validation technique used by industry up to today, but remain error prone and expensive cost. Automatically generating test cases from formal models of the system under test is a promising improvement approach to cut down the testing cost. This paper introduces a technique that automatically generate real-time conformance test cases from timed automata specifications. First, both reactive system and its environment is modeled by restricted automata with the notion of deterministic, input enabled and output urgent. Then demonstration is given to show how to efficiently generate real-time test cases with optimal execution time from diagnostic trace. Finally, we formally specify user's single purpose or coverage criteria to convert the test case generation problem into a reachability problem. This approach is implemented using model checkers as test case generation tools and experiment results on three different coverage criteria specifications show feasibility and effectiveness of our technique.