Soltanieh | Compositional Stochastic Process Algebra Models: A Focus on Model Repair and Rate Lifting | Buch | 978-3-8439-5332-0 | sack.de

Buch, Englisch, 174 Seiten, Paperback, Format (B × H): 170 mm x 240 mm, Gewicht: 335 g

Reihe: Informatik

Soltanieh

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


Erscheinungsjahr 2023
ISBN: 978-3-8439-5332-0
Verlag: Dr. Hut

Buch, Englisch, 174 Seiten, Paperback, Format (B × H): 170 mm x 240 mm, Gewicht: 335 g

Reihe: Informatik

ISBN: 978-3-8439-5332-0
Verlag: Dr. Hut


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.

Soltanieh Compositional Stochastic Process Algebra Models: A Focus on Model Repair and Rate Lifting jetzt bestellen!

Autoren/Hrsg.




Ihre Fragen, Wünsche oder Anmerkungen
Vorname*
Nachname*
Ihre E-Mail-Adresse*
Kundennr.
Ihre Nachricht*
Lediglich mit * gekennzeichnete Felder sind Pflichtfelder.
Wenn Sie die im Kontaktformular eingegebenen Daten durch Klick auf den nachfolgenden Button übersenden, erklären Sie sich damit einverstanden, dass wir Ihr Angaben für die Beantwortung Ihrer Anfrage verwenden. Selbstverständlich werden Ihre Daten vertraulich behandelt und nicht an Dritte weitergegeben. Sie können der Verwendung Ihrer Daten jederzeit widersprechen. Das Datenhandling bei Sack Fachmedien erklären wir Ihnen in unserer Datenschutzerklärung.