Abstract
Unified Modeling Language (UML) is considered a standard for modeling object-oriented software. It supports several different diagrams that can be used to model behavior and structure of the software. With respect to formal verification, particularly Model Checking, the existing approaches are usually restricted to a single UML diagram. This paper presents a tool to convert UML behavioral diagrams (sequence, activity, and state machine) into Transition Systems to support software Model Checking. A peculiar feature of our tool is that it is developed as part of a larger effort to allow Model Checking of software built in accordance with UML, including several UML behavioral diagrams. We demonstrate the effectiveness of our approach by applying it to a classic case study and also to a real case study (embedded software) in the space domain.
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
Baier, C., Katoen, J.P.: Principles of model checking, p. 975. The MIT Press, Cambridge (2008)
Schäfer, T., Knapp, A., Merz, S.: Model checking uml state machines and collaborations. Electronic Notes in Theoretical Computer Science 55(3), 357–369 (2001)
OMG, T.O.M.G.: Omg - unified modeling language (omg uml) (1997)
Debbabi, M., Hassaïne, F., Jarraya, Y., Soeanu, A., Alawneh, L.: Verification and Validation in Systems Engineering, p. 270. Springer, Heidelberg (2010)
Eshuis, R., Wieringa, R.: Tool support for verifying uml activity diagrams. IEEE Transactions on Software Engineering 30(7), 437–447 (2004)
Sarma, M., Mall, R.: Automatic generation of test specifications for coverage of system state transitions. Information and Software Technology 51(2), 418–432 (2009)
Pressman, R.S.: Software Engineering: A Practitioner’s Approach, 7th edn. McGrawHill, New York (2010)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the International Conference on Software Engineering (ICSE), pp. 411–420. ACM Press, New York (1999)
Cockburn, A.: Writing Effective Use Cases, p. 304. Addison-Wesley Professional, US (2000)
Kessler, F.B.: Nusmv home page (2011)
eclipse.org: Papyrus (2014)
Holzmann, G.: The SPIN model checker: Primer and reference manual, vol. 1003. Addison-Wesley (2004)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
eclipse.org: Eclipse (2014)
Santiago, V., Mattiello-Francisco, M., Costa, R., Silva, W., Ambrosio, A.: Qsee project: an experience in outsourcing software development for space applications. In: The 19th International Conference on Software Engineering & Knowledge Engineering (SEKE), pp. 51–56 (2007)
Mikk, E., Lakhnech, Y., Siegel, M., Holzmann, G.: Implementing statecharts in promela/spin. In: Proceedings. 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques, pp. 90–101. IEEE (1998)
Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of uml statechart diagrams using the spin model-checker. Formal Aspects of Computing 11(6), 637–664 (1999)
Lam, V.: A formalism for reasoning about uml activity diagrams. Nordic Journal of Computing 14(1), 43–64 (2007)
Dubrovin, J., Junttila, T.: Symbolic model checking of hierarchical uml state machines. In: ACSD 2008. 8th International Conference on Application of Concurrency to System Design, pp. 108–117. IEEE (2008)
Uchitel, S., Kramer, J.: A workbench for synthesising behaviour models from scenarios. In: Proceedings of the 23rd Intern. Conference on Software Engineering, pp. 188–197. IEEE Computer Society (2001)
Baresi, L., Morzenti, A., Motta, A., Rossi, M.: Towards the UML-based formal verification of timed systems. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects. LNCS, vol. 6957, pp. 267–286. Springer, Heidelberg (2011)
Cortellessa, V., Mirandola, R.: Prima-uml: a performance validation incremental methodology on early uml diagrams. Science of Computer Programming 44(1), 101–129 (2002)
Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: Practice and experience. ACM Computing Surveys 41(4), 19:1–19:36 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
dos Santos, L.B.R., Eras, E.R., de Santiago Júnior, V.A., Vijaykumar, N.L. (2014). A Formal Verification Tool for UML Behavioral Diagrams. In: Murgante, B., et al. Computational Science and Its Applications – ICCSA 2014. ICCSA 2014. Lecture Notes in Computer Science, vol 8579. Springer, Cham. https://doi.org/10.1007/978-3-319-09144-0_48
Download citation
DOI: https://doi.org/10.1007/978-3-319-09144-0_48
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-09143-3
Online ISBN: 978-3-319-09144-0
eBook Packages: Computer ScienceComputer Science (R0)