Show simple item record

2021-09-15Dissertation DOI: 10.18452/23310
Quantitative Modeling and Verification of Evolving Software
dc.contributor.authorGetir Yaman, Sinem
dc.date.accessioned2021-09-15T10:28:25Z
dc.date.available2021-09-15T10:28:25Z
dc.date.issued2021-09-15none
dc.identifier.urihttp://edoc.hu-berlin.de/18452/24000
dc.description.abstractMit der steigenden Nachfrage nach Innovationen spielt Software in verschiedenenWirtschaftsbereichen eine wichtige Rolle, wie z.B. in der Automobilindustrie, bei intelligenten Systemen als auch bei Kommunikationssystemen. Daher ist die Qualität für die Softwareentwicklung von großer Bedeutung. Allerdings ändern sich die probabilistische Modelle (die Qualitätsbewertungsmodelle) angesichts der dynamischen Natur moderner Softwaresysteme. Dies führt dazu, dass ihre Übergangswahrscheinlichkeiten im Laufe der Zeit schwanken, welches zu erheblichen Problemen führt. Dahingehend werden probabilistische Modelle im Hinblick auf ihre Laufzeit kontinuierlich aktualisiert. Eine fortdauernde Neubewertung komplexer Wahrscheinlichkeitsmodelle ist jedoch teuer. In letzter Zeit haben sich inkrementelle Ansätze als vielversprechend für die Verifikation von adaptiven Systemen erwiesen. Trotzdem wurden bei der Bewertung struktureller Änderungen im Modell noch keine wesentlichen Verbesserungen erzielt. Wahrscheinlichkeitssysteme werden als Automaten modelliert, wie bei Markov-Modellen. Solche Modelle können in Matrixform dargestellt werden, um die Gleichungen basierend auf Zuständen und Übergangswahrscheinlichkeiten zu lösen. Laufzeitmodelle wie Matrizen sind nicht signifikant, um die Auswirkungen von Modellveränderungen erkennen zu können. In dieser Arbeit wird ein Framework unter Verwendung stochastischer Bäume mit regulären Ausdrücken entwickelt, welches modular aufgebaut ist und eine aktionshaltige sowie probabilistische Logik im Kontext der Modellprüfung aufweist. Ein solches modulares Framework ermöglicht dem Menschen die Entwicklung der Änderungsoperationen für die inkrementelle Berechnung lokaler Änderungen, die im Modell auftreten können. Darüber hinaus werden probabilistische Änderungsmuster beschrieben, um eine effiziente inkrementelle Verifizierung, unter Verwendung von Bäumen mit regulären Ausdrücken, anwenden zu können. Durch die Bewertung der Ergebnisse wird der Vorgang abgeschlossen.ger
dc.description.abstractSoftware 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. Due to the dynamic nature of modern software systems, probabilistic models representing the quality of the software 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 represented in a matrix form to solve the equations based on states and transition probabilities. On the other side, evolutionary changes can create various effects on theese models and force them 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.eng
dc.language.isoengnone
dc.publisherHumboldt-Universität zu Berlin
dc.rights(CC BY 4.0) Attribution 4.0 Internationalger
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/
dc.subjectProbabilistische Verifikationger
dc.subjectprobabilistische Modellprüfungger
dc.subjectstochastische reguläre Ausdrückeger
dc.subjectprobabilistische reguläre Ausdrückeger
dc.subjectinkrementelle Verifikationger
dc.subjectSoftwarequalitätger
dc.subjectZuverlässigkeitger
dc.subjectPerformanceger
dc.subjectsoftware Evolutionger
dc.subjectSystemsicherheitger
dc.subjectProbabilistic verificationeng
dc.subjectprobabilistic model checkingeng
dc.subjectstochastic regular expressionseng
dc.subjectprobabilistic regular expressionseng
dc.subjectincremental verificationeng
dc.subjectsoftware evolutioneng
dc.subjectsoftware qualityeng
dc.subjectreliabilityeng
dc.subjectperformanceeng
dc.subjectsystem safetyeng
dc.subject.ddc000 Informatik, Informationswissenschaft, allgemeine Werkenone
dc.titleQuantitative Modeling and Verification of Evolving Softwarenone
dc.typedoctoralThesis
dc.identifier.urnurn:nbn:de:kobv:11-110-18452/24000-2
dc.identifier.doihttp://dx.doi.org/10.18452/23310
dc.date.accepted2021-06-25
dc.contributor.refereeGrunske, Lars
dc.contributor.refereeTichy, Matthias
dc.contributor.refereeSchlingloff, Holger
local.edoc.pages181none
local.edoc.type-nameDissertation
local.edoc.institutionMathematisch-Naturwissenschaftliche Fakultätnone
dc.relation.references10.3233/FI-2021-2018
dc.relation.references10.3233/FI-2021-2018

Show simple item record