The Taub Faculty of Computer Science Events and Talks

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 UML models. We will shortly describe other approaches for verifying behavioral UML systems, developed as part of this thesis.