Quantitative modeling and verification of evolving software
Başlık çevirisi mevcut değil.
- Tez No: 721203
- Danışmanlar: PROF. DR. SABİNE KUNST, PROF. DR. ELMAR KULKE
- Tez Türü: Doktora
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Bilim ve Teknoloji, Computer Engineering and Computer Science and Control, Science and Technology
- Anahtar Kelimeler: Probabilistic verification, probabilistic model checking, stochastic regular expressions, probabilistic regular expressions, incremental verification, software evolution, software quality, reliability, performance, system safety
- Yıl: 2021
- Dil: İngilizce
- Üniversite: Humboldt-Unıversıtat Zu Berlın
- Enstitü: Yurtdışı Enstitü
- Ana Bilim Dalı: Belirtilmemiş.
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: Belirtilmemiş.
Özet
Mit der steigenden Nachfrage nach Innovationen spielt Software in verschiedenen Wirtschaftsbereichen eine wichtige Rolle, wie z.B. in der Automobilindustrie, bei autonomen und intelligenten Systemen als auch bei Kommunikationssystemen. Daher ist die Qualität für die Softwareentwicklung von großer Bedeutung. Es wurden verschiedene Ansätze entwickelt, um die Qualitätsmerkmale von Systemen wie Zuverlässigkeit, Sicherheit (Safety) und Performance von Software zu bewerten. In der Regel dienen Modelle wie z.B. die der Markov-Modelle, Fehlerbäume und Petri-Netze als Modelle der Software, die für die Erstellung der verschiedenen Auswertungsverfahren ausschlaggebend sind. Normalerweise enthalten diese Modelle Entwurfszeitschätzungen für bestimmte Übergangswahrscheinlichkeiten, die zur Laufzeit auf ihre Genauigkeit überprüft werden müssen. Allerdings ändern sich diese Modelle angesichts der dynamischen Natur moderner Softwaresysteme. Dies führt dazu, dass ihre Übergangswahrscheinlichkeiten im Laufe der Zeit schwanken, welches zu erheblichen Problemen führt. Um korrekte Bewertungsergebnisse quantitativer Eigenschaften erhalten zu können, müssen diese gelöst werden. 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 mit Wahrscheinlichkeitsdaten modelliert, wie bei Markov-Modellen, Markov-Entscheidungsprozessen und probabilistischen Automaten. Auch werden algebraische Sprachen wie stochastische Algebren wie Differentialgleichungen auf Basis von Markov-Ketten analysiert. Solche Modelle können in Matrixform dargestellt werden, um die Gleichungen basierend auf Zuständen und Übergangswahrscheinlichkeiten zu lösen. Auf der anderen Seite können solche Änderungen auch verschiedene Auswirkungen auf die Modelle haben oder eine erneute Überprüfung des gesamten Systemmodells erzwingen. Laufzeitmodelle wie Matrizen oder Diagrammdarstellungen 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.
Özet (Çeviri)
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.
Benzer Tezler
- Denizcilik sektöründe sera gazı emisyonu önlemlerinin etki değerlendirmesinin sistem dinamikleriyle modellenmesi
System dynamics modelling of the impact assessment of greenhouse gas mitigation measures in maritime transportation
SELEN UYGUR
Doktora
Türkçe
2025
Denizcilikİstanbul Teknik ÜniversitesiDeniz Ulaştırma İşletme Mühendisliği Ana Bilim Dalı
DOÇ. DR. PELİN BOLAT
- Bir atık barajının sismik yükler ve sürekli yağış etkisinde dinamik analizinin değerlendirilmesi
Evaluation of dynamic analysis of tailings dam under the effect of seismic loads and continuous rainfall
HASAN ÇELT
Yüksek Lisans
Türkçe
2025
Maden Mühendisliği ve Madencilikİstanbul Teknik ÜniversitesiMaden Mühendisliği Ana Bilim Dalı
PROF. DR. ATAÇ BAŞÇETİN
- Sürdürülebilir finans ve SKDM arasındaki ilişki: Politika etki değerlendirmesi ve bir çimento tesisi varsayımsal vaka analizi
The relationship between sustainable finance and the CBAM: A policy impact assessment and hypothetical case study of a cement plant
İNCİ NUR ÇETİN
Yüksek Lisans
Türkçe
2025
Çevre Mühendisliğiİstanbul Teknik ÜniversitesiÇevre Mühendisliği Ana Bilim Dalı
PROF. DR. SADULLAH LEVENT KUZU
- Ortaokul 7. sınıf öğrencilerinin matematiksel modelleme ve epistemolojik inançları üzerine bir çalışma
A study on mathematical modeling competencies and epistemological beliefs of the 7th grade students
RECEP DİNÇ
Yüksek Lisans
Türkçe
2020
Eğitim ve ÖğretimDicle ÜniversitesiMatematik ve Fen Bilimleri Eğitimi Ana Bilim Dalı
DR. ÖĞR. ÜYESİ MEHMET AYDIN
- Addie öğretim tasarımının 9. sınıf öğrencilerinin matematiksel modelleme, iletişim, mantıksal düşünme ve motivasyonuna etkisi
The effect of the Addie instructional design on mathematical modeling, communication, logical thinking and motivation of grade 9 students
İPEK GÜNDÜZ ÇETİN
Doktora
Türkçe
2024
Eğitim ve ÖğretimAydın Adnan Menderes ÜniversitesiEğitim Programları ve Öğretim Ana Bilim Dalı
PROF. DR. ASUMAN SEDA SARACALOĞLU