From Scenarios to Test Implementations Via Promela

  • Andreas Ulrich
  • El-Hachemi Alikacem
  • Hesham H. Hallal
  • Sergiy Boroday
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6435)


We report on a tool for generating executable concurrent tests from scenarios specified as message sequence charts. The proposed approach features three steps: 1) Deriving a MSC test implementation from a MSC scenario, 2) Mapping the test implementation into a Promela model, 3) Generating executable test scripts in Java. The generation of an intermediate Promela model allows for model-checking to inspect the test implementation for properties like soundness, fault detection power as well as for consistency checking between different test scenarios. Moreover decoupling the executable test scripts from the scenario specification makes it possible to use different backend code generators to support other scripting languages when needed.


Scenario-based testing distributed testing test consistency Promela Message Sequence Charts UML2 sequence diagrams tool implementation 


  1. 1.
    Neto, A.D., Subramanyan, R., Vieira, M., Travassos, G.H., Shull, F.: Improving Evidence about Software Technologies – A Look at Model-Based Testing. IEEE Software 24, 10–13 (2008)CrossRefGoogle Scholar
  2. 2.
    Haugen, O.: Comparing UML 2.0 Interactions and MSC-2000. In: Amyot, D., Williams, A.W. (eds.) SAM 2004. LNCS, vol. 3319, pp. 69–84. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  3. 3.
    OMG UML Specification,
  4. 4.
    Boroday, S., Petrenko, A., Ulrich, A.: Implementing MSC Tests with Quiescence Observation. In: Núñez, M. (ed.) TESTCOM/FATES 2009. LNCS, vol. 5826, pp. 235–238. Springer, Heidelberg (2009)Google Scholar
  5. 5.
    Ulrich, A.: Introducing Model-Based Testing Techniques in Industrial Projects. In: GI-Edition. LNI, Proc. Bd., vol. 106, pp. 29–34 (2007)Google Scholar
  6. 6.
    Baker, P., Bristow, P., Jervis, C., King, D., Mitchell, W.: Automatic Generation of Conformance Tests from Message Sequence Charts. In: Sherratt, E. (ed.) SAM 2002. LNCS, vol. 2599, pp. 170–198. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)Google Scholar
  8. 8.
    Boroday, S., Petrenko, A., Ulrich, A.: Test Suite Consistency Verification. In: 6th IEEE East-West Design & Test Symposium (EWDTS 2008), pp. 235–238 (2008)Google Scholar
  9. 9.
    Grabowski, J., Koch, B., Schmitt, M., Hogrefe, D.: SDL and MSC Based Test Generation for Distributed Test Architectures. In: SDL Forum 1999, pp. 389–404 (1999)Google Scholar
  10. 10.
    Mitchell, B.: Lazy Buffer Semantics for Partial Order Scenarios. In: Automated Software Engineering, vol. 14, pp. 419–441. Springer, Heidelberg (2007)Google Scholar
  11. 11.
    Holzmann, G., Peled, D., Redberg, M.: Design Tools for Requirement Engineering. Bell Labs Technical. J. 2, 86–95 (1997)CrossRefGoogle Scholar
  12. 12.
    Papesch, M.: Generating Implementations from Formal Specifications: A Translator from Promela to Java. Student thesis no 1826. University of Stuttgart (2002)Google Scholar
  13. 13.
    de Jonge, M.: The SpinJ Model Checker. Master’s Thesis. University of TwenteGoogle Scholar
  14. 14.
    ANTLR Parser Generator,

Copyright information

© IFIP International Federation for Information Processing 2010

Authors and Affiliations

  • Andreas Ulrich
    • 1
  • El-Hachemi Alikacem
    • 2
  • Hesham H. Hallal
    • 3
  • Sergiy Boroday
    • 2
  1. 1.Corporate TechnologySiemens AGMunichGermany
  2. 2.CRIMMontrealCanada
  3. 3.Lebanese International UniversityBeirutLebanon

Personalised recommendations