|Title:||Learning-Based Compositional Model Checking of Behavioral UML Systems
|Authors:||Yael Meller, Orna Grumberg, and Karen Yorav
|Currently accessibly only within the Technion network|
|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.
|Copyright||The above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information|
Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2015/CS/CS-2015-05), rather than to the URL of the PDF files directly. The latter URLs may change without notice.
To the list of the CS technical reports of 2015
To the main CS technical reports page
Computer science department, Technion