Efficient test case generation for validation of UML activity diagrams

摘要

Unified Modeling Language (UML) is widely used as a system level specification language in embedded system design. Due to the increasing complexity of embedded systems, the analysis and validation of UML specifications is becoming a challenge. UML activity diagram is promising to modeling the overall system behavior. However, lack of techniques for automated test case generation is one major bottleneck in the UML activity diagram validation. This article presents a methodology for automatically generating test cases based on various model checking techniques. It makes three primary contributions: First, we propose coverage-driven mapping rules that can automatically translate activity diagram to formal models. Next, we present a procedure for automatic property generation according to error models. Finally, we apply various model checking based test case generation techniques to enable efficient test case generation. Our experimental results demonstrate that our approach can reduce the validation effort drastically by reducing both test case generation time and required number of test cases to achieve a functional coverage goal.