Kompositionale Analyse Komponenten-basierter Systeme mittels Cross-Checking

点击翻译按钮获取中文摘要

Dieser Antrag hat den Nachweis generischer Eigenschaften kooperierender Prozesse zum Thema. Beispiele für solche Eigenschaften sind globale/lokale Deadlock- Freiheit, Lebendigkeit oder Fortschritt. Das hier vorgestellte Projekt behandelt eine Vorgehensweise, die in Kombination mit anderen Verfahren wie Deduktive Programmverifikation, Abstrakte Interpretation, Hinreichende Bedingungen, Model-Checking und Äquivalenzen dazu beitragen soll, dass Systeme mit sehr großem Zustandsraum einer Überprüfung unterzogen werden können. Wir konzentrieren uns auf den Nachweis von Eigenschaften für Komponenten-basierte Systeme als Teilklasse von kooperierenden Systemen. Dabei liegt die folgende Sicht von Komponenten-basierten Systemen zugrunde: eine Komponente ist eine Einheit, die eine gewisse Funktionalität besitzt und unabhängig vom Kontext ihres Einsatzes entwickelt wird. Eine Komponente hat kein Wissen über andere Komponenten. Komponenten werden mittels eines separaten Glue-Codes zusammengesetzt. Dies ermöglicht uns auf kompositionale Weise Informationen über das Gesamtsystem durch die Untersuchung von Teilsystemen zu erlangen.