Humboldt-Universität zu Berlin - Mathematisch-Naturwissenschaftliche Fakultät - Software Engineering

Frau Sinem Getir wird in Kürze ihre Dissertation zum Thema

"PROBABILISTIC VERIFICATION AND MODELLING OF EVOLVING SOFTWARE" an unserer Fakultät einreichen.

Alle Interessierten sind ganz herzlich zu ihrem Probevortrag eingeladen!

Abstract

Software plays an innovative role in many different domains such as car industry; autonomous and smart systems; communication; among others. Hence, the quality of the software is of utmost importance and needs to be properly addressed during software evolution.

Several approaches have been developed to evaluate systems’s quality attributes like reliability, safety and performance of software. Commonly, models such as Markov models, fault trees, and Petri-nets serve as models of the software to be built for different evaluation procedures. Usually these models contain design time estimates for specific transition probabilities, which have to be checked at runtime for their accurateness. Furthermore, due to the dynamic nature of modern software systems, these models and their transition probabilities change over time and fluctuate, leading to a significant problem that need to be solved to obtain correct evaluation results of quantitative properties. To solve this issue, probabilistic models need to be continually updated at runtime. However, continuous re-evaluation of complex probabilistic models is expensive. Recently, incremental approaches have been found to be promising for the verification of evolving and self-* systems. Nevertheless, substantial improvements have not yet been achieved for evaluating structural changes in the model.

Probabilistic systems are usually modelled as automata with probabilisticdata. e.g. Markov chains, Markov Decision Processes, probabilistic automata. Even algebraic languages like stochastic algebras are analysed on the underlying models like Markov chains. Such models can be represented in matrix form to solve the equations based on states and transition probabilities. On the other side, such changes can create various effects on the models or force to analyse re-verifying the whole system. Runtime models such as matrixes or graph representations lack the expressiveness to identify the change effect on the model.

In this thesis, we develop a framework using stochastic regular expression trees, which are modular, with action based probabilistic logic in the model checking context. After formal foundations of model checking framework, we develop edit operations to analyse SRE model for the incremental computation of local changes that can occur in the model to cope with this problem. Furthermore, we describ probabilistic change patterns to apply efficient incremental verification using regular expression trees and evaluated our results.