The Taub Faculty of Computer Science Events and Talks
Yael Meller (Ph.D. Thesis Seminar)
Wednesday, 17.06.2015, 11:30
Advisor: Prof. Orna Grumberg and Dr. Karen Yorav
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 given system satisfies a desired
property. It is widely recognized as an important approach to increase the
reliability of hardware and software systems and is vastly used in industry.
Unfortunately, the applicability of model checking is often impeded by its high
time and memory requirements, referred to as the state explosion problem.
In this talk I will present our work on learning-based compositional verification
of behavioral UML models. Compositional verification is a successful approach
for fighting the state explosion problem. Recently, great advancements have been
made in this direction via automatic learning-based Assume-Guarantee reasoning.
We present a framework for automatic Assume-Guarantee reasoning of behavioral UML
models. We apply an off-the-shelf learning algorithm for incrementally generating
assumptions on the systems' environment, 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
We will shortly describe other approaches for verifying behavioral UML systems,
developed as part of this thesis.