Model-based Automatic Test Generation for Event-Driven Embedded Systems using Model Checkers

Testing is an essential, but time and resource consuming activity in the software development process. In the case of model-based development, among other subtasks test construction and test execution can be partially automated. Our paper describes the implementation of a test generator framework that uses an external model checker to construct test sequences. The possible configurations of the model checker are examined by measuring the efficiency of test construction in the case of different statechart models of event-driven embedded systems. The generated test cases are transformed and executed on common testing frameworks (JUnit, rational robot) and the effectiveness of tests are measured using code coverage metrics