Software & Systems Modeling

, Volume 16, Issue 2, pp 393–415 | Cite as

Language-specific model checking of UML-RT models

Special Section Paper
  • 197 Downloads

Abstract

Model-driven development (MDD) deals with complexities of modern software development by using models. Their verification is one of the opportunities of MDD, since it can be performed in the early stages of the development. The prevailing trend in verification of MDD models has been to translate them to an input language of one of the existing tools, most notably model checkers. Such an approach has advantages; for instance, we can use tools that achieved a higher level of maturity, including SPIN, NuSMV and Java PathFinder. However, the input languages of model checkers are typically not compatible with MDD models, which can make the translations very complex and difficult to maintain. Moreover, it is more difficult to take advantage of specific features of the structure and semantics of models to, e.g., speed up analysis. In this paper, we depart from the translational trend and present more direct and dedicated approach. We use an MDD language, namely UML-RT (used in IBM Rational Software Architect RealTime Edition), and we introduce a verification method built around its main features such as hierarchical structures, action code and asynchronous communication. In our method we use a formalization tailored to UML-RT models. This enables very easy transformation of models, but also reduces the necessary translations of verification results and directly supports the most important features of UML-RT. The proposed method includes an on-the-fly model checking algorithm based on the original CTL labeling. This algorithm is further optimized to include lazy composition. In the paper, we present all necessary components of the checking algorithms. Additionally, we also show the results of experiments with our implementation using several UML-RT models and CTL formulas. The experiments provide some evidence of the viability of a language-specific analysis of MDD models and of the effectiveness of our optimizations in certain cases.

Keywords

UML-RT Model checking Lazy composition 

References

  1. 1.
    Balasubramanian, D., Păsăreanu, C.S., Karsai, G., Lowry, M.R.: Polyglot: systematic analysis for multiple statechart formalisms. In: Piterman, N., Smolka, S.A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 523–529. Springer, Berlin (2013)Google Scholar
  2. 2.
    Bhat, G., Cleaveland, R., Grumberg, O.: Efficient on-the-fly model checking for CTL. In: Symposium on Logic in Computer Science, pp. 388–397. IEEE, New York (1995)Google Scholar
  3. 3.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  4. 4.
    Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: Logic in Computer Science LICS, pp. 353–362 (1989)Google Scholar
  5. 5.
    Concrete syntax for a UML action language: Action Language for Foundational UML (ALF). http://www.omg.org/spec/ALF/. Last accessed 21 June 2014
  6. 6.
    Compton, K., Gurevich, Y., Huggins, J., Shen, W.: An automatic verification tool for UML. Technical report, University of Michigan (2000)Google Scholar
  7. 7.
    Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. In: Kurshan, R. (ed.) Computer-Aided Verification, pp. 129–142. Springer, Berlin (1993)Google Scholar
  8. 8.
    Giese, H., Tichy, M., Burmester, S., Schäfer, W., Flake, S.: Towards the compositional verification of real-time UML designs. In: Proceedings of the ESEC/FSE, pp. 38–47 (2003)Google Scholar
  9. 9.
    Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E.M., Kurshan, R.P. (eds.) Computer-Aided Verification, pp. 186–196. Springer, Berlin (1991)Google Scholar
  10. 10.
    Hammer, M., Knapp, A., Merz, S.: Truly on-the-fly LTL model checking. In: Halbwachs, N., Zuck, L.D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 191–205. Springer, Berlin (2005)Google Scholar
  11. 11.
  12. 12.
    IBM rational software architect, realtime edition, version 8.0.2. http://publib.boulder.ibm.com/infocenter/. Last accessed 21 June 2014
  13. 13.
    Jensen, H.E., Larsen, G.K., Skou, A.: Scaling up uppaal. In: Joseph, M. (ed.) Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 641–678. Springer, Berlin (2000)Google Scholar
  14. 14.
    Jussila, T., Dubrovin, J., Junttila, T., Latvala, T., Porres, I.: Model checking dynamic and hierarchical UML state machines. In: Proceedings of the 3rd Workshop on Model Design and Validation MoDeVa, pp. 94–110 (2006)Google Scholar
  15. 15.
    Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Form. Asp. Comput. 11(6), 637–664 (1999)CrossRefMATHGoogle Scholar
  16. 16.
    Leue, S., Stefanescu, A., Wei, W.: An AsmL semantics for dynamic structures and run time schedulability in UML-RT. Technical report, University of Konstanz, Konstanz (2008)Google Scholar
  17. 17.
    Lind-Nielsen, J., Andersen, H.R., Hulgaard, H., Behrmann, G., Kristoffersen, K., Larsen, K.G.: Verification of large state/event systems using compositionality and dependency analysis. Form. Methods Syst. Des. 18(1), 5–23 (2001)CrossRefMATHGoogle Scholar
  18. 18.
    Mehlitz, P.C.: Trust your model–verifying aerospace system models with Java pathfinder. In: IEEE Aerospace Conference (2008)Google Scholar
  19. 19.
    Posse, E., Dingel, J.: An executable formal semantics for UML-RT. Softw. Syst. Model. 1–39 (2014)Google Scholar
  20. 20.
    Saaltink, M., Meisels, I.: Using SPIN to analyse RoseRT models. Technical report, ORA Canada (1999)Google Scholar
  21. 21.
    Schäfer, T., Knapp, A., Merz, S.: Model checking UML state machines and collaborations. Electron. Notes Theor. Comput. Sci. 55(3), 1–13 (2001)CrossRefGoogle Scholar
  22. 22.
    Selic, B., Gullekson, G., Ward, P.T.: Real-Tme Object Oriented Modeling and Design. Wiley, London (1994)MATHGoogle Scholar
  23. 23.
    Shen, W., Compton, K., Huggins, J.: A UML validation toolset based on abstract state machines. In: International Conference on Automated Software Engineering, pp. 315–318 (2001)Google Scholar
  24. 24.
    Unified Modeling Language (UML 2.0) superstructure. http://www.uml.org/. Last accessed 21 June 2014
  25. 25.
    Vergauwen, B., Lewi, J.: A linear local model checking algorithm for CTL. In: CONCUR, pp. 447–461. Springer, Berlin (1993)Google Scholar
  26. 26.
    Visser, W., Dwyer, M.B., Whalen, M.: The hidden models of model checking. Softw. Syst. Model. 11(4), 541–555 (2012)Google Scholar
  27. 27.
    Zheng, H.: Compositional reachability analysis for efficient modular verification of asynchronous designs. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 29(3), 329–340 (2010)Google Scholar
  28. 28.
    Zurowska, K.: Language specific analysis of state machine models of reactive systems. Ph.D. thesis, Queen’s Univerity, Canada (2014)Google Scholar
  29. 29.
    Zurowska, K., Dingel, J.: Symbolic execution of communicating and hierarchically composed UML-RT state machines. In: Goodloe, A.E., Person, S. (eds.) NASA Formal Methods, pp. 39–53. Springer, Berlin (2012)Google Scholar
  30. 30.
    Zurowska, K., Dingel, J.: Model checking of UML-RT models using lazy composition. In: MoDELS, pp. 304–319 (2013)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  1. 1.School of ComputingQueen’s UniversityKingstonCanada

Personalised recommendations