Verifikation quantitativer Eigenschaften eines Mikrokernbetriebssystems durch eine Kombination von probabilistischem Model Checking und interaktivem Theorembeweisen

Die langfristige Vision der Antragsteller ist Die konstrudens modernen Mikrokerns, fr r zum enderen enformaler, fr r zum enderder nachweers zentrer Eigenschaften erbracht, d r zum anderen alle Funktionalität besitzt, Die in hetigen, realen Anwendungsszenarien benötigt werden。[4] [1] [1] [1] [1] [1] [1] [1] [1] [1] [1] [1] [1] [1] [1] [4]2 .德国德国德国德国德国德国德国德国德国德国德国德国德国德国德国德国德国德国德国德国德国Typische Beispiele solch定量定量Anforderungen sind die Zusicherung， dass einen erfolgreichen Zugriff auf eine Sperrvariable mit einer Wahrscheinlichkeit von 1−10−6 nicht mehr als drei Versuche benötigt werden oder auth die Forderung， dass die Reaktionszeit auf eine anstehende Unterbrechung在98%以上Fälle höchstens 2 μs beträgt。求解特征schaften steen在工程中的应用。因此，技术上的严格要求是定量的、可量化的、可量化的、可量化的。在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国，在德国。Ein Beispielen hierf<e:1> r - 1 die Dekodierung eines Videodatenstroms。[j] [Nachweis solcher Eigenschaften - forfordere - technik - technik - Antragsteller], nämlich betriebssystem and formale verification .]因此，从编程代码ausgehende，提取，提取，验证，过程，数学，模型，分析，模型，分析，函数，定量，特征特征，特征特征，特征特征，特征特征，特征特征，特征特征，特征特征。Der zu erwartende erkentnisgewinde projects list vielfältig。在此基础上，提出了一种新的方法，可用于分析复杂系统的非均质结构、非均质结构、非均质结构、非均质结构、非均质结构、非均质结构、非均质结构、非均质结构和非均质结构。Ferner erwartenwir， dass durchchfhhrdbetrtrten项目，包括新erkententenisen与概率方案模型检验的理论结合，以及erkententenisen与模型检验、标准化与分析随机分析（Echtzeit-）系统寿命分析。

Die langfristige Vision der Antragsteller ist die Konstruktion eines modernen Mikrokerns, für den zum einen ein formaler, vom Programmcode ausgehender Nachweis zentraler Eigenschaften erbracht wird, und der zum anderen alle Funktionalität besitzt, die in heutigen, realen Anwendungsszenarien benötigt werden. Der Schwerpunkt der ersten Projektphase liegt auf der Entwicklung von Methoden für die Modellierung und Analyse, die für den Nachweis der relevanten Eigenschaften geeignet sind. Die nachzuweisenden Eigenschaften sollen dabei neben funktionaler Korrektheit vor allem quantitative Anforderungen, wie etwa Aussagen über Ausfallwahrscheinlichkeiten oder Reaktionszeiten, umfassen. Typische Beispiele solch quantitativer Anforderungen sind die Zusicherung, dass für einen erfolgreichen Zugriff auf eine Sperrvariable mit einer Wahrscheinlichkeit von 1−10−6 nicht mehr als drei Versuche benötigt werden oder auch die Forderung, dass die Reaktionszeit auf eine anstehende Unterbrechung in 98% aller Fälle höchstens 2 μs beträgt. Solche Eigenschaften stehen in engem Zusammenhang mit der Optimierung von Mikrokernen. So rechtfertigt z.B. die zuerst genannte quantitative Anforderung die Verwendung hochperformanter, jedoch unfairer Locks. Die Verwendung von weichen Echtzeitbedingungen, wie mit der zweitgenannten Eigenschaft angedeutet, ist sinnvoll in Umgebungen, in denen im Mittel eine hohe Dienstgüte unbedingt sichergestellt werden muß, jedoch das gelegentliche Nichteinhalten der Dienstgüte hinnehmbar ist. Ein Beispielen hierfür ist die Dekodierung eines Videodatenstroms. Der Nachweis solcher Eigenschaften erfordert eine nichttriviale Kombination von Methoden der jeweiligen Forschungsgebiete der Antragsteller, nämlich Betriebssysteme und formale Verifikation. Sowohl eine vom Programmcode ausgehende Extraktion eines für den Verifikationsprozess geeigneten mathematischen Modells als auch die Analyse des Modells hinsichtlich funktionaler und quantitativer Eigenschaften stellen wissenschaftliche Herausforderungen dar. Der zu erwartende Erkenntnisgewinn des Projekts ist vielfältig. Wir gehen davon aus, dass unsere Arbeiten zu einer prinzipiell einsetzbaren Methodik für die funktionale und quantitative Analyse und Optimierung von Betriebssystemkernen führen werden, die auch auf andere komplexe Systeme mit einer heterogenen Struktur aus Hard- und Softwarekomponenten anwendbar ist. Ferner erwarten wir, dass die Durchführung des beantragten Projekts auch neue Erkenntnisse hinsichtlich der Kombination von Theorembeweisen und probabilistischem Model Checking und hinsichtlich der Modellierung, Spezifikation und Analyse stochastischer (Echtzeit-)Systeme liefern wird.