ISBN 9783843953320

978-3-8439-5332-0, Reihe Informatik

Amin Soltanieh
Compositional Stochastic Process Algebra Models: A Focus on Model Repair and Rate Lifting

174 Seiten, Dissertation Universität der Bundeswehr München (2022), Softcover, B5

Zusammenfassung / Abstract

Modelling, analysis, and verification are the first steps to improving the reliability, availability, and thus the usefulness of a concurrent system. Probabilistic model checking is a widely used verification technique for checking the quantitative properties of stochastic systems. When a model does not satisfy a property, a model repair method can modify the model to positively affect the satisfaction probability. This work addresses probabilistic model checking and model repair of concurrent systems, specified with the help of Stochastic Process Algebra (SPA) models.

This thesis consists of two major parts: the first part studies the compositional approach to perform model checking and model repair of a specific type of product-form model (Boucherie framework). In this approach, the compositional structure of the system is exploited, and it is a well-established method to tackle the notorious state space explosion problem.

The second part focuses on the Rate Lifting problem which provides a different perspective compared to earlier works on model repair, making it a significant contribution: The user, who always works with the high-level SPA specification, can now directly obtain the model repair information for the high-level SPA model. The introduced algorithms execute the process of rate lifting for an arbitrary number of interacting components with arbitrary synchronising structure. Whenever necessary, the algorithms change the synchronisation of the SPA model and insert artificial controlling selfloops at distinct states, but in such a way that the model's underlying transition system is preserved. Having to deal with the complex synchronisation structure of multi-component models made it necessary to identify some new structural and behavioral properties of SPA, referring to the high-level model as well as to the low-level model. The multi-component rate lifting algorithm is then developed based on these properties of SPA models.