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

Sinem Getir will give a test presentation of her PhD defense on the topic: Quantitative Modeling and Verification of Evolving Software

Abstract:

Software plays an innovative role in many different domains, such as car industry, autonomous and smart systems, and communication. 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’ quality attributes, such as reliability, safety, and performance of software. Models, such as Markov models, fault trees, and Petri nets, commonly serve as models of the software to be built for different evaluation procedures. These models usually contain design-time estimates for specific transition probabilities, which have to be checked at run-time 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 needs to be solved to obtain correct evaluation results of quantitative properties. Probabilistic models need to be continually updated at run-time to solve this issue. 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-adaptive systems. Nevertheless, substantial improvements have not yet been achieved for evaluating structural changes in the model.

Probabilistic systems are usually modeled as automata with probabilistic data (e.g., Markov chains, Markov Decision Processes, probabilistic  automata). Even algebraic languages, such as stochastic algebras, are analyzed on the underlying models like Markov chains. Such models can be represented in a 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 and force one to re-verify the whole system. Run-time models, such as matrices 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. Such a modular framework enables us to develop change operations for the incremental computation of local changes that can occur in the model. Furthermore, we describe probabilistic change patterns to apply efficient incremental quantitative verification using stochastic regular expression trees and evaluate our results.

Die Zugangsdaten zum Zoom Onlinemeeting teilt Hoang Lam Nguyen gern auf Anfrage mit.