Abstract
This work presents a novel approach for applying abstraction and refinement in the verification of behavioral UML models.
The Unified Modeling Language (UML) is a widely accepted modeling language for embedded and safety critical systems. As such the correct behavior of systems represented as UML models is crucial. Model checking is a successful automated verification technique for checking whether a system satisfies a desired property. Nevertheless, its applicability is often impeded by its high time and memory requirements. A successful approach to avoiding this limitation is CounterExample-Guided Abstraction-Refinement (CEGAR). We propose a CEGAR-like approach for UML systems. We present a model-to-model transformation that generates an abstract UML system from a given concrete one, and formally prove that our transformation creates an over-approximation.
The abstract system is often much smaller, thus model checking is easier. Because the abstraction creates an over-approximation we are guaranteed that if the abstract model satisfies the property then so does the concrete one. If not, we check whether the resulting abstract counterexample is spurious. In case it is, we automatically refine the abstract system, in order to obtain a more precise abstraction.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Majzik, I., Darvas, A., Beny, B.: Verification of UML statechart models of embedded systems. In: DDECS 2002 (2002)
Booch, G., Rumbaugh, J.E., Jacobson, I.: The unified modeling language user guide. J. Database Manag. 10(4), 51–52 (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), 498–520 (1998)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. Journal of the ACM 50(5), 752–794 (2003)
Clarke, E.M., Heinle, W.: Modular translation of statecharts to SMV. Tr, CMU (2000)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)
Damm, W., Josko, B., Pnueli, A., Votintseva, A.: Understanding UML: A formal semantics of concurrency and communication in real-time UML. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 71–98. Springer, Heidelberg (2003)
Dubrovin, J., Junttila, T.A.: Symbolic model checking of hierarchical UML state machines. In: ACSD 2008 (2008)
Fecher, H., Huth, M., Schmidt, H., Schönborn, J.: Refinement sensitive formal semantics of state machines with persistent choice. Electron. Notes Theor. Comput. Sci. 250(1), 71–86 (2009)
Fecher, H., Schönborn, J.: UML 2.0 state machines: Complete formal semantics via core state machine. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol. 4346, pp. 244–260. Springer, Heidelberg (2007)
Object Management Group. OMG Unified Modeling Language (UML) Infrastructure, version 2.4. ptc/2010-11-16 (2010)
Grumberg, O., Meller, Y., Yorav, K.: Applying software model checking techniques for behavioral UML models. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 277–292. Springer, Heidelberg (2012)
Gurfinkel, A., Chechik, M.: Why waste a perfectly good abstraction? In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 212–226. Springer, Heidelberg (2006)
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), 637–664 (1999)
Liu, S., Liu, Y., André, É., Choppy, C., Sun, J., Wadhwa, B., Dong, J.S.: A formal semantics for complete UML state machines with communications. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 331–346. Springer, Heidelberg (2013)
Madhukar, K., Metta, R., Singh, P., Venkatesh, R.: Reachability verification of rhapsody statecharts. In: ICSTW 2013 (2013)
Meller, Y., Grubmerg, O., Yorav, K.: Verifying behavioral UML systems via CEGAR. TR CS-2014-01, Dept. of Computer Science. Technion - Israel Institute of Technology (2014)
Mikk, E., Lakhnech, Y., Siegel, M., Holzmann, G.J.: Implementing statecharts in promela/spin. In: WIFT 1998 (1998)
Ober, I., Graf, S., Ober, I.: Validating timed UML models by simulation and verification. STTT 8(2), 128–145 (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 (1977)
Prehofer, C.: Behavioral refinement and compatibility of statechart extensions. Electron. Notes Theor. Comput. Sci. 295(5), 65–78 (2013)
Reeve, G., Reeves, S.: Logic and refinement for charts. In: ACSC 2006 (2006)
Schinz, I., Toben, T., Mrugalla, C., Westphal, B.: The rhapsody UML verification environment. In: SEFM 2004 (2004)
Scholz, P.: Incremental design of statechart specifications. Sci. Comput. Program. 40(1), 119–145 (2001)
Seger, C.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Form. Methods Syst. Des. 6(2), 147–189 (1995)
Simons, A.J.H., Stannett, M.P., Bogdanov, K.E., Holcombe, W.M.L.: Plug and play safely: Rules for behavioural compatibility. In: SEA 2002 (2002)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Meller, Y., Grumberg, O., Yorav, K. (2014). Verifying Behavioral UML Systems via CEGAR. In: Albert, E., Sekerinski, E. (eds) Integrated Formal Methods. IFM 2014. Lecture Notes in Computer Science(), vol 8739. Springer, Cham. https://doi.org/10.1007/978-3-319-10181-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-10181-1_9
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10180-4
Online ISBN: 978-3-319-10181-1
eBook Packages: Computer ScienceComputer Science (R0)