Abstract
This work presents a novel approach for the verification of Behavioral UML models, by means of software model checking.
We propose adopting software model checking techniques for verification of UML models. We translate UML to verifiable C code which preserves the high level structure of the models, and abstracts details that are not needed for verification. We combine of static analysis and bounded model checking for verifying LTL safety properties and absence of livelocks.
We implemented our approach on top of the bounded software model checker CBMC. We compared it to an IBM research tool that verifies UML models via a translation to IBM’s hardware model checker RuleBasePE. Our experiments show that our approach is more scalable and more robust for finding long counterexamples. We also demonstrate the usefulness of several optimizations that we introduced into our tool.
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
Majzik, I., Darvas, A., Beny, B.: Verification of UML Statechart Models of Embedded Systems. In: DDECS (2002)
Armando, A., Mantovani, J., Platania, L.: Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers. STTT 11(1) (2009)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Booch, G., Rumbaugh, J.E., Jacobson, I.: The Unified Modeling Language User Guide. J. Database Manag. 10(4) (1999)
Chan, W., Anderson, R.J., Beame, P., Burns, S., Modugno, F., Notkin, D., Reese, J.D.: Model Checking Large Software Specifications. IEEE Trans. Software Eng. 24(7) (1998)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)
Clarke, E.M., Heinle, W.: Modular Translation of Statecharts to SMV. Technical Report, CMU (2000)
Clarke, E., Kroning, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-Based Bounded Model Checking for Embedded ANSI-C Software. In: ASE (2009)
Csertán, G., Huszerl, G., Majzik, I., Pap, Z., Pataricza, A., Varró, D.: VIATRA - Visual Automated Transformations for Formal Verification and Validation of UML Models. In: ASE (2002)
Dubrovin, J., Junttila, T.A.: Symbolic Model Checking of Hierarchical UML State Machines. In: ACSD (2008)
Object Management Group. OMG Unified Modeling Language (UML) Infrastructure, version 2.4. ptc/2010-11-16 (2010)
Harel, D.: Statecharts: A Visual Formalism for Complex Systems. Sci. Comp. Prog. 8(3) (1987)
Jussila, T., Dubrovin, J., Junttila, T., Latvala, T., Porres, I.: Model Checking Dynamic and Hierarchical UML State Machines. In: MoDeVa (2006)
Kaveh, N.: Using Model Checking to Detect Deadlocks in Distributed Object Systems. In: Emmerich, W., Tai, S. (eds.) EDO 2000. LNCS, vol. 1999, pp. 116–128. Springer, Heidelberg (2001)
Latella, D., Majzik, I., Massink, M.: Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker. Formal Asp. Comput. 11(6) (1999)
Mikk, E., Lakhnech, Y., Siegel, M., Holzmann, G.J.: Implementing Statecharts in PROMELA/SPIN. In: WIFT (1998)
Ober, I., Graf, S., Ober, I.: Validating Timed UML Models by Simulation and Verification. STTT 8(2) (2006)
IST-2001-33522 OMEGA (2001), http://www-omega.imag.fr
Lilius, J., Paltor, I.P.: Formalising UML State Machines for Model Checking. In: France, R.B. (ed.) UML 1999. LNCS, vol. 1723, pp. 430–444. Springer, Heidelberg (1999)
Pnueli, A.: The Temporal Logic of Programs. In: FOCS (1977)
Prashanth, C.M., Shet, K.C., Elamkulam, J.: An Efficient Event Based Approach for Verification of UML Statechart Model for Reactive Systems. In: ADCOM (2008)
RuleBasePE, http://www.haifa.ibm.com/projects/verification/RB_Homepage/
Schinz, I., Toben, T., Mrugalla, C., Westphal, B.: The Rhapsody UML Verification Environment. In: SEFM (2004)
Sheeran, M., Singh, S., Stålmarck, G.: Checking Safety Properties Using Induction and a SAT-Solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)
Sistla, A.P.: Safety, Liveness and Fairness in Temporal Logic. Formal Asp. Comput. 6(5) (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grumberg, O., Meller, Y., Yorav, K. (2012). Applying Software Model Checking Techniques for Behavioral UML Models. In: Giannakopoulou, D., Méry, D. (eds) FM 2012: Formal Methods. FM 2012. Lecture Notes in Computer Science, vol 7436. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32759-9_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-32759-9_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32758-2
Online ISBN: 978-3-642-32759-9
eBook Packages: Computer ScienceComputer Science (R0)