Learning-Based Compositional Model Checking of Behavioral UML Systems
| Autor: | Orna Grumberg, Yael Meller, Karen Yorav |
|---|---|
| Rok vydání: | 2016 |
| Předmět: | |
| Zdroj: | Formal Aspects of Component Software ISBN: 9783319289335 FACS |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|