Abstract
This work presents a novel approach for applying compositional model checking of behavioral UML models, based on learning. 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. However, its applicability is often impeded by its high time and memory requirements. A successful approach to tackle this limitation is compositional model checking. Recently, great advancements have been made in this direction via automatic learning-based Assume-Guarantee reasoning.
In this work we propose a framework for automatic Assume-Guarantee reasoning for behavioral UML systems. We apply an off-the-shelf learning algorithm for incrementally generating environment assumptions that guarantee satisfaction of the property. A unique feature of our approach is that the generated assumptions are UML state machines. Moreover, our Teacher works at the UML level: all queries from the learning algorithm are answered by generating and verifying behavioral UML systems.
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.
An extended version including full proofs is published as a technical report in [22].
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 subscriptionsNotes
- 1.
The case where several state machines run on the same thread is simpler, however presentation of both is cumbersome. We present only the more complex case.
- 2.
In the examples throughout the paper we assume EQs are implemented as FIFOs.
- 3.
In LTL, the syntax of this property is AGp. We choose to denote it by \(\forall Gp\) in order to differentiate the property from AG (which stands for Assume-Guarantee).
- 4.
It is ok to require p on a prefix leading to state err, since \(A_w\) is prefix closed for safety properties.
References
Majzik, I., Darvas, A., Beny, B.: Verification of UML statechart models of embedded systems. In: Design and Diagnostics of Electronic Circuits and Systems Workshop (DDECS 2002), pp. 70–77. IEEE (2002)
Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987)
Booch, G., Rumbaugh, J.E., Jacobson, I.: The unified modeling language user guide. J. Database Manag. 10(4), 51–52 (1999)
Strichman, O., Chaki, S.: Optimized L*-based assume-guarantee reasoning. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 276–291. Springer, Heidelberg (2007)
Chan, W., Anderson, R.J., Beame, P., Burns, S., Modugno, F., Notkin, D., Reese, J.D.: Model checking large software specifications. IEEE Trans. Softw. Eng. 24(7), 498–520 (1998)
Chen, Y.-F., Tsay, Y.-K., Clarke, E.M., Farzan, A., Wang, B.-Y.: Learning minimal separating DFA’s for compositional verification. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 31–45. Springer, Heidelberg (2009)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT press, Cambridge (1999)
Clarke, E.M., Heinle, W.: Modular translation of statecharts to SMV. Technical report CMU-CS-00-XXX, Carnegie-Mellon University School of Computer Science (2000)
Cobleigh, J.M., Giannakopoulou, D., Păsăreanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)
Dubrovin, J., Junttila, T.A.: Symbolic model checking of hierarchical UML state machines. In: Application of Concurrency to System Design (ACSD 2008), pp. 108–117. IEEE (2008)
Farzan, A., Tsay, Y.-K., Chen, Y.-F., Wang, B.-Y., Clarke, E.M.: Extending automated compositional verification to the full class of omega-regular languages. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 2–17. Springer, Heidelberg (2008)
Giannakopoulou, D., Păsăreanu, C.S., Barringer, H.: Component verification with automatically generated assumptions. Autom. Softw.Eng. 12(3), 297–320 (2005)
Object Management Group. OMG Unified Modeling Language (UML) Superstructure, version 2.4.1. formal/2011-08-06 (2011)
Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. 16(3), 843–871 (1994)
Meller, Y., Yorav, K., Grumberg, O.: 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)
Gupta, A., McMillan, K.L., Fu, Z.: Automated assumption generation for compositional verification. Form. Methods Syst. Des. 32(3), 285–301 (2008)
Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)
Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Form. Methods Syst. Des. 19(3), 291–314 (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), 637–664 (1999)
Madhukar, K., Metta, R., Singh, P., Venkatesh, R.: Reachability verification of rhapsody statecharts. In: International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2013), pp. 96–101. IEEE (2013)
Grumberg, O., Meller, Y., Yorav, K.: Verifying behavioral UML systems via CEGAR. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 139–154. Springer, Heidelberg (2014)
Meller, Y., Grumberg, O., Yorav, K.: Learning-based compositional model checking of behavioral UML systems. Technical report CS-2015-05, Department of Computer Science, Technion - Israel Institute of Technology (2015)
Mikk, E., Lakhnech, Y., Siegel, M., Holzmann, G.J.: Implementing statecharts in PROMELA/SPIN. In: Workshop on Industrial-Strength Formal Specification Techniques (WIFT 1998), pp. 90–101. IEEE (1998)
Nam, W., Madhusudan, P., Alur, R.: Automatic symbolic compositional verification by learning assumptions. Form. Methods Syst. Des. 32(3), 207–234 (2008)
Pasareanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Form. Methods Syst. Des. 32(3), 175–205 (2008)
Pnueli, A.: The temporal logic of programs. In: Proceedings of the Eighteenth Annual Symposium on Foundations of Computer Science (FOCS 1977) (1977)
Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K.R. (ed.) Formal Models of Concurrent Systems, pp. 123–144. Springer-Verlag, Berlin (1985)
Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. In: Symposium on Theory of Computing (STOC 1989), pp. 411–420. ACM (1989)
Schinz, I., Toben, T., Mrugalla, C., Westphal, B.: The rhapsody UML verification environment. In: Software Engineering and Formal Methods (SEFM 2004), pp. 174–183. IEEE (2004)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Meller, Y., Grumberg, O., Yorav, K. (2016). Learning-Based Compositional Model Checking of Behavioral UML Systems. In: Braga, C., Ölveczky, P. (eds) Formal Aspects of Component Software. FACS 2015. Lecture Notes in Computer Science(), vol 9539. Springer, Cham. https://doi.org/10.1007/978-3-319-28934-2_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-28934-2_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-28933-5
Online ISBN: 978-3-319-28934-2
eBook Packages: Computer ScienceComputer Science (R0)