Name
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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-319-28934-2_15 | FACS |
Field | DocType | Volume |
UML state machine,Programming language,Model checking,Unified Modeling Language,UML tool,Computer science,Modeling language,Finite-state machine,Applications of UML,Object Constraint Language | Conference | 9539 |
ISSN | Citations | PageRank |
0302-9743 | 1 | 0.35 |
References | Authors | |
13 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yael Meller | 1 | 5 | 1.10 |
| Orna Grumberg | 2 | 4361 | 351.99 |
| Karen Yorav | 3 | 479 | 32.67 |