Kompositionale Spezifikation und Verifikation paralleler Programme

Zentrales Problem beim Einsatz automatischer Verifikationsmethoden zur Verifikation großer Hard- und Softwaresysteme ist das Problem der Zustandsexplosion. In der Praxis der Software-Entwicklung hat es sich bewährt, komplexe Systeme aus Teilsystemen ("Agenten") überschaubarer Komplexität mit wohldefinierten Schnittstelle und klarer Abgrenzung der Verantwortlichkeiten zusammenzusetzen. Im Rahmen dieses Projekts wird eine Übertragung dieser Vorgehensweise auf den Bereich der formalen Methoden untersucht. Dies beinhaltet die Untersuchung verschiedener Kompositionskonzepte, die u.a. aus Techniken der objektorientierten Entwicklung motiviert sind.

Spezielle Fragestellungen betreffen:

Assumption-commitment-Regeln zum kompositionalen Schließen über Komponenten
Logiken zum Schließen über nebenläufige Systeme
Abstraktionstechniken
Computergestützte Analyseverfahren wie model checking oder interaktives Theorembeweisen und deren Integration

Das Projekt wurde teilweise vom DAAD im Rahmen des PROCOPE-Programms gefördert.

Projektpartner: Applied Logics Group, Institut de recherche en informatique de Toulouse

Ansprechpartner: Dr. Stephan Merz

Veröffentlichungen:

Liste aller Projekte

Institut

Universität