zbMATH — the first resource for mathematics

Applying software model checking techniques for behavioral UML models. (English) Zbl 1372.68171
Giannakopoulou, Dimitra (ed.) et al., FM 2012: Formal methods. 18th international symposium, Paris, France, August 27–31, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32758-2/pbk). Lecture Notes in Computer Science 7436, 277-292 (2012).
Summary: 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.
For the entire collection see [Zbl 1250.68029].
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI