Abstract
We present a fully automated approach to verifying safety properties of Executable UML models (xUML). Our tool chain consists of a model transformation program which translates xUML models to the process algebra mCRL2, followed by symbolic model checking using LTSmin. If a safety violation is found, an error trace is visualised as a UML sequence diagram. As a novel feature, our approach allows safety properties to be specified as UML state machines.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM Transactions on Programming Languages and Systems 23(3), 273–303 (2001)
ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state/event-based model-checking approach for the analysis of abstract system properties. Science of Computer Programming 76(2), 119–135 (2011)
Behrmann, G., Larsen, K.G., Andersen, H.R., Hulgaard, H., Lind-Nielsen, J.: Verification of hierarchical state/event systems using reusability and compositionality. Formal Methods in System Design 21(2), 225–244 (2002)
Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Information and Control 60(1-3), 109–137 (1984)
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers 58, 118–149 (2003)
Blom, J., Hessel, A., Jonsson, B., Pettersson, P.: Specifying and generating test cases using observer automata. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 125–139. Springer, Heidelberg (2005)
Blom, S., van de Pol, J., Weber, M.: LTSmin: Distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354–359. Springer, Heidelberg (2010)
Ciardo, G., Lüttgen, G., Miner, A.S.: Exploiting interleaving semantics in symbolic state-space generation. Formal Methods in System Design 31(1), 63–100 (2007)
Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D., Torielli, F., Traverso, P.: Formal verification of a railway interlocking system using model checking. Formal Aspects of Computing 10(4), 361–380 (1998)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM 50(5), 752–794 (2003)
Damm, W., Josko, B., Pnueli, A., Votintseva, A.: A discrete-time UML semantics for concurrency and communication in safety-critical applications. Science of Computer Programming 55, 81–155 (2005)
Eriksson, L.-H.: Specifying railway interlocking requirements for practical use. In: Proceedings of the 15th International Conference on Computer Safety, Reliability and Security (SAFECOMP 1996). Springer, Heidelberg (1996)
Fokkink, W.: Safety criteria for the vital processor interlocking at Hoorn-Kersenboogerd. In: Computers in Railways V (COMPRAIL 1996). Railway Systems and Management, vol. I (1996)
Formal Systems (Europe) Ltd. Failures-divergence refinement: FDR2 User Manual (2010)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: A toolbox for the construction and analysis of distributed processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372–387. Springer, Heidelberg (2011)
Geilen, M.: On the construction of monitors for temporal logic properties. Electr. Notes in Theor. Comp. Sci. 55(2) (2001)
Ghazel, M., Toguyéni, A., Yim, P.: State observer for DES under partial observation with timed petri nets. Discrete Event Dynamic Systems 19(2), 137–165 (2009)
Gnesi, S., Latella, D., Lenzini, G., Abbaneo, C., Amendola, A.M., Marmo, P.: An automatic SPIN validation of a safety critical railway control system. In: Proceedings of the 2000 Int. Conf. on Dependable Systems and Networks, pp. 119–124. IEEE Computer Society, Washington, DC, USA (2000)
Graw, G., Herrmann, P.: Transformation and verification of Executable UML models. In: Proceedings of the Workshop on the Compositional Verification of UML Models. Electr. Notes in Theor. Comp. Sci, vol. 101, pp. 3–24 (2004)
Groote, J.F., Mathijssen, A., Reniers, M.A., Usenko, Y.S., van Weerdenburg, M.: The formal specification language mCRL2. In: Methods for Modelling Software Systems. Dagstuhl Seminar Proceedings, vol. 06351 (2007)
Hansen, H.H., Ketema, J., Luttik, B., Mousavi, M.R., van de Pol, J.: Towards model checking Executable UML specifications in mCRL2. Innovations in Systems and Software Engineering 6(1-2), 83–90 (2010)
Heidenreich, F., Johannes, J., Karol, S., Seifert, M., Wende, C.: Derivation and refinement of textual syntax for models. In: Paige, R.F., Hartman, A., Rensink, A. (eds.) ECMDA-FA 2009. LNCS, vol. 5562, pp. 114–129. Springer, Heidelberg (2009), http://www.emftext.org (last visit: July 4, 2011)
Hoare, T.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley, Reading (2003)
ISO/IEC. Enhancements to Lotos (E-Lotos), International Standard 15437:2001 (2001)
ISO/IEEE. ISO/IEEE 11073-20601: Health infomatics — personal health device communication — Part 20601: Application profile — optimized exchange protocol (April 2010)
Keiren, J.: Modelling session setup of IEEE Std 11073-20601 (2011), Personal communication
KnowGravity. Cassandra/xUML User’s Guide (2008)
Kolovos, D.: An Extensible Platform for Specification of Integrated Languages for Model Management. PhD thesis, University of York, United Kingdom (2009), http://www.eclipse.org/gmt/epsilon/ (last visit: July 4, 2011)
Kolovos, D., Rose, L., Paige, R.: The Epsilon Book, http://www.eclipse.org/gmt/epsilon/doc/book/ (last visit: July 4, (2011)
Lafortune, S., Teneketzis, D., Sampath, M., Sengupta, R., Sinnamohideen, K.: Failure diagnosis of dynamic systems: an approach based on discrete event systems. In: Proceedings of the American Control Conference, vol. 3, pp. 2058–2071 (2001)
Lind-Nielsen, J., Andersen, H.R., Hulgaard, H., Behrmann, G., Kristoffersen, K.J., Larsen, K.G.: Verification of large state/event systems using compositionality and dependency analysis. Formal Methods in System Design 18(1), 5–23 (2001)
Mekki, A., Ghazel, M., Toguyeni, A.: Time-constrained systems validation using MDA model transformation. A railway case study. In: Proceedings of the 8th International Conference of Modeling and Simulation, MOSIM 2010 (2010)
Mellor, S.J., Balcer, M.: Executable UML: A foundation for model-driven architecture. Addison-Wesley, Reading (2002)
Object Management Group. OMG Unified Modeling Language Superstructure Version 2.2 (February 2009)
Papyrus Developers. Papyrus: Open source tool for graphical UML2 modelling, http://www.papyrusuml.org (last visit: July 4, 2011)
Schneider, F.B.: Enforceable security policies. ACM Transactions on Information and Systems Security 3(1), 30–50 (2000)
Sheeran, M., Stålmarck, G.: A tutorial on stålmarck’s proof procedure for propositional logic. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 82–99. Springer, Heidelberg (1998)
Sighireanu, M.: LOTOS NT user’s manual. Technical report, INRIA Rhône-Alpes/VASY (2008)
Steinberg, D., Budinsky, F., Paternostro, M., Merks, E.: EMF: Eclipse Modeling Framework. Addison-Wesley Professional, Boston (2008), http://www.eclipse.org/modeling/emf/ (last visit: July 4, 2011)
Turner, E., Treharne, H., Schneider, S., Evans, N.: Automatic generation of CSP || B skeletons from xUML models. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 364–379. Springer, Heidelberg (2008)
Winter, K., Robinson, N.J.: Modelling large railway interlockings and model checking small ones. In: ACSC 2003: Proceedings of the 26th Australasian Comp. Sci. Conference, pp. 309–316. Australian Computer Society, Inc. (2003)
Yeung, W.L., Leung, K.R.P.H., Wang, J., Dong, W.: Improvements towards formalizing UML state diagrams in CSP. In: Proceedings of the 12th Asia-Pacific Software Engineering Conference (APSEC 2005). IEEE Computer Society, Los Alamitos (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hvid Hansen, H., Ketema, J., Luttik, B., Mousavi, M., van de Pol, J., dos Santos, O.M. (2011). Automated Verification of Executable UML Models. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds) Formal Methods for Components and Objects. FMCO 2010. Lecture Notes in Computer Science, vol 6957. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25271-6_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-25271-6_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25270-9
Online ISBN: 978-3-642-25271-6
eBook Packages: Computer ScienceComputer Science (R0)