Logo des Repositoriums
 
Textdokument

Maschinelle Verifikation von parametrisierten Echtzeitsystemen

Vorschaubild nicht verfügbar

Volltext URI

Dokumententyp

Zusatzinformation

Datum

2013

Zeitschriftentitel

ISSN der Zeitschrift

Bandtitel

Verlag

Gesellschaft für Informatik

Zusammenfassung

Sicherheitskritische Echtzeitsysteme umfassen häufig nicht nur eine statische, sondern eine parametrisierte, beliebig große Anzahl von nebenläufigen Prozessen. Ein Echtzeitbetriebssystem z.B. verwaltet beliebig viele Threads. Solche Systeme enthalten prinzipiell zwei Quellen von Unendlichkeit: Es existieren einerseits unendlich viele Systeminstanzen, die andererseits durch die Betrachtung von Echtzeit jeweils einen unendlich großen Zustandsraum besitzen. Mit formaler Verifikation kann die Korrektheit in allen Systemabläufen nachgewiesen werden. Dies ist jedoch für derartige unendliche Systeme mit komplexen Systemstrukturen automatisch prinzipiell nicht möglich. Bisher fehlt es an maschinellen, teilautomatisierten Verifikationsansätzen, die weiterhin die Korrektheit von Beweisen selbst sicherstellen. Um dies zu ermöglichen, haben wir ein Rahmenwerk entwickelt, das die Verifikation in einem interaktiven Theorembeweiser erlaubt. Dadurch können Teilbeweise automatisiert werden und es wird sichergestellt, dass (möglicherweise kritische) Randfälle nicht übersehen werden können.Um den damit verbundenen interaktiven Verifikationsaufwand zu reduzieren, ermöglichen wir es weiterhin, Systeminstanzen automatisch zu validieren. Damit können eventuelle Gegenbeispiele vor der Verifikation im Theorembeweiser genutzt werden, um das parametrisierte Gesamtsystem entsprechend zu korrigieren.

Beschreibung

Göthel, Thomas (2013): Maschinelle Verifikation von parametrisierten Echtzeitsystemen. Ausgezeichnete Informatikdissertationen 2012. Bonn: Gesellschaft für Informatik. PISSN: 1617-5468. ISBN: 978-3-88579-417-2. pp. 121-130

Schlagwörter

Zitierform

DOI

Tags