Design Automation for Embedded Systems

, Volume 14, Issue 2, pp 105–130 | Cite as

Efficient test case generation for validation of UML activity diagrams

  • Mingsong Chen
  • Prabhat Mishra
  • Dhrubajyoti Kalita


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.


UML activity diagram Testing Model checking Property decomposition 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Rumbaugh J, Jacobson I, Booch G (2001) The unified modeling language user guide. Addison-Wesley, Boston Google Scholar
  2. 2.
    OMG (2007) UML superstructure V2.1.2. Available at
  3. 3.
    Martin G (2002) UML for embedded systems specification and design: motivation and overview. In: Design automation and test in Europe 2005, pp 773–775 Google Scholar
  4. 4.
    Martin G, Müller W (2005) UML for SOC design. Springer, Berlin CrossRefGoogle Scholar
  5. 5.
    Müller W, Rosti A, Bocchio S, Riccobene E, Scandurra P, Dehaene W, Vanderperren Y (2006) UML for ESL design–basic principles, tools, and applications. In: International conference on computer-aided design 2006, pp 73–80 Google Scholar
  6. 6.
    Peterson J (1981) Petri nets theory and the modeling of systems. Prentice-Hall, New York Google Scholar
  7. 7.
    Chen M, Mishra P, Kalita D (2008) Coverage-driven automatic test generation for UML activity diagrams. In: Proceedings of Great Lakes symposium of VLSI (GLSVLSI), pp 139–142 Google Scholar
  8. 8.
    Ammann P, Black P, Majurski W (1998) Using model checking to generate tests from specifications. In: Proceedings of international conference on formal engineering methods (ICFEM), pp 46–54 Google Scholar
  9. 9.
    Bryant RE (1986) Graph-based algorithms for Boolean function manipulations. IEEE Trans Comput 35(8):677–691 MATHCrossRefGoogle Scholar
  10. 10.
    Prasad M, Biere A, Gupta A (2005) A survey of recent advances in SAT-based formal verification. Int J Softw Tools Technol Transf 7(2):156–173 CrossRefGoogle Scholar
  11. 11.
    Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: International conference on tools and algorithms for the construction and analysis of systems, pp 193–207 Google Scholar
  12. 12.
    Riccobene E, Scandurra P, Rosti A, Bocchio S (2005)A SoC design methodology involving a UML 2.0 profile for SystemC. In: Design automation and test in Europe, pp 704–709 Google Scholar
  13. 13.
    Müller W, Rosti A, Bocchio S, Riccobene E, Scandurra P, Dehaene W, Vanderperren Y (2006) UML for ESL design: basic principles, tools, and applications. In: International conference on computer aided design, pp 73–80 Google Scholar
  14. 14.
    Rosenberg D, Mancerella S (2010) Embedded systems development using SysML: an illustrated example using enterprise architect. Sparx Systems Pty Ltd and ICONIX Google Scholar
  15. 15.
    Lamberg K (2007) Trends and perspectives in automated ECU testing. In: Automotive electronic, June, 2007 Google Scholar
  16. 16.
  17. 17.
    Lavagno L, Müller W (2006) UML as a next-generation language for SoC design. In: Electronic design Google Scholar
  18. 18.
    Heckel R, Lohmann M (2003) Towards model-driven testing. In: International workshop on test and analysis of component based systems, pp 284–291 Google Scholar
  19. 19.
    Briand LC, Labiche Y (2002) A UML-based approach to system testing. Softw System Model 1(1):10–42 CrossRefGoogle Scholar
  20. 20.
    Chen T, Poon P, Tang S, Tse T (2005) Identification of categories and choices in activity diagrams. In: International conference on software quality 2005, pp 55–63 Google Scholar
  21. 21.
    Wang L, Yuan J, Yu X, Hu J, Li X, Zheng G (2004) Generating test cases from UML activity diagram based on gray-box method. In: Asia-pacific software engineering conference 2004, pp 284–291 Google Scholar
  22. 22.
    Kim H, Kang S, Baik J, Ko I (2007) Test cases generation from UML activity diagrams. In: Software engineering, artificial intelligence, networking, and parallel/distributed computing 2007, pp 556–561 Google Scholar
  23. 23.
    Chen M, Qiu X, Li X (2006) Automatic test case generation for UML activity diagrams. In: International workshop on automation on software test 2006, pp 2–8 Google Scholar
  24. 24.
    Chen M, Qiu X, Xu W, Wang L, Zhao J, Li X (2009) UML activity diagram based automatic test case generation for Java programs. Comput J 52(5):545–556 CrossRefGoogle Scholar
  25. 25.
    Unhelkar B (2005) Verification and validation for quality of UML 2.0 models. Wiley, New York CrossRefGoogle Scholar
  26. 26.
    Bell A, Haverkort BR (2005) Sequential and distributed model checking of Petri nets. Int J Softw Tools Technol Transf 7(1):43–60 CrossRefGoogle Scholar
  27. 27.
    Jensen K, Kristensen LM, Wells L (2007) Coloured Petri nets and CPN tools for modelling and validation of concurrent systems. Int J Softw Tools Technol Transf 9(3–4):213–254 CrossRefGoogle Scholar
  28. 28.
    Eshuis R (2006) Symbolic model checking of UML activity diagrams. ACM Trans Softw Eng Methodol 15(1):1–38 CrossRefGoogle Scholar
  29. 29.
    Cimatti A, Clarke EM, Giunchiglia F, Roveri M (1999) NUSMV: a new symbolic model verifier. In: International conference on computer aided verification 1999, pp 495–499 Google Scholar
  30. 30.
    Guelfi N, Mammar A (2005) A formal semantics of timed activity diagrams and its PROMELA translation. In: Asia-Pacific software engineering conference 2005, pp 283–290 Google Scholar
  31. 31.
    Das D, Kumar R, Chakrabarti PP (2006) Timing verification of UML activity diagram based code block level models for real time multiprocessor system-on-chip applications. In: Asia-Pacific software engineering conference 2006, pp 199–208 Google Scholar
  32. 32.
    Chen M, Mishra P, Kalita D (2007) RTL towards test generation from systemc TLM specifications. In: High level design validation and test workshop 2007, pp 91–96 Google Scholar
  33. 33.
    Fraser G, Wotawa F (2007) Improving model-checkers for software testing. In: International conference on software quality 2007, pp 25–31 Google Scholar
  34. 34.
    Mishra P, Dutt N (2005) Functional coverage driven test generation for validation of pipelined processors. In: Design automation and test in Europe 2005, pp 678–683 Google Scholar
  35. 35.
    Koo H, Mishra P (2006) Functional test generation using property decompositions for validation of pipelined processors. In: Design automation and test in Europe, pp 1240–1245 Google Scholar
  36. 36.
    Mishra P, Chen M (2009) Efficient techniques for directed test generation using incremental satisfiability. In: International conference on VLSI design, pp 65–70 Google Scholar
  37. 37.
    Chen M, Qin X, Mishra P (2010) Efficient decision ordering techniques for SAT-based test generation. In: Design, automation and test in Europe, pp 490–495 Google Scholar
  38. 38.
    Chen M, Mishra P (2010) Functional test generation using efficient property clustering and learning techniques. IEEE Tran Comput-Aided Des Integr Circuits Syst 29(3):396–404 CrossRefGoogle Scholar
  39. 39.
    Rayadurgam S, Heimdahl MPE (2001) Coverage based test-case generation using model checkers. In: International conference and workshop on the engineering of computer based systems 2001, pp 83–91 Google Scholar
  40. 40.
    Clarke EM, Grumberg O, Peled DA (2000) Model checking. MIT Press, Cambridge Google Scholar
  41. 41.
    Marques-Silva J, Sakallah K (1999) GRASP: A search algorithm for propositional satisfiability. IEEE Trans Comput 48(5):506–521 CrossRefMathSciNetGoogle Scholar
  42. 42.
    Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: Engineering an efficient SAT solver. In: Design automation conference, pp 530–535 Google Scholar
  43. 43.
    Ericsson M (2004) Activity diagrams: What they are and how to use them. The Rational Edge Google Scholar
  44. 44.
    Zhu H, Hall P, May J (1997) Software unit test coverage and adequacy. ACM Comput Surv 29(4):366–427 CrossRefGoogle Scholar
  45. 45.
    McMillan KL Cadence SMV. Available at
  46. 46.
    Reshadi M, Gorjiara B, Dutt N (2006) Generic processor modeling for automatically generating very fast cycle-accurate simulators. IEEE Trans CAD Integr Circuits Syst 25(12):2904–2918 CrossRefGoogle Scholar
  47. 47.
    Hennessy J, Patterson D (2003) Computer architecture: a quantitative approach. Morgan Kaufmann, San Mateo Google Scholar

Copyright information

© Springer Science+Business Media, LLC 2010

Authors and Affiliations

  • Mingsong Chen
    • 1
  • Prabhat Mishra
    • 1
  • Dhrubajyoti Kalita
    • 2
  1. 1.Department of Computer & Information Science & EngineeringUniversity of FloridaGainesvilleUSA
  2. 2.Intel CorporationFolsomUSA

Personalised recommendations