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. © 2012 Springer-Verlag.
CITATION STYLE
Grumberg, O., Meller, Y., & Yorav, K. (2012). Applying software model checking techniques for behavioral UML models. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7436 LNCS, pp. 277–292). https://doi.org/10.1007/978-3-642-32759-9_25
Mendeley helps you to discover research relevant for your work.