Logo des Repositoriums
 

Maschinelle Verifikation von parametrisierten Echtzeitsystemen

dc.contributor.authorGöthel, Thomas
dc.contributor.editorHölldobler, Steffen
dc.date.accessioned2020-08-21T08:45:57Z
dc.date.available2020-08-21T08:45:57Z
dc.date.issued2013
dc.description.abstractSicherheitskritische 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.de
dc.identifier.isbn978-3-88579-417-2
dc.identifier.pissn1617-5468
dc.identifier.urihttps://dl.gi.de/handle/20.500.12116/33727
dc.language.isode
dc.publisherGesellschaft für Informatik
dc.relation.ispartofAusgezeichnete Informatikdissertationen 2012
dc.relation.ispartofseriesLecture Notes in Informatics (LNI) - Dissertations, Volume D-13
dc.titleMaschinelle Verifikation von parametrisierten Echtzeitsystemende
gi.citation.endPage130
gi.citation.publisherPlaceBonn
gi.citation.startPage121

Dateien

Originalbündel
1 - 1 von 1
Vorschaubild nicht verfügbar
Name:
121.pdf
Größe:
241.27 KB
Format:
Adobe Portable Document Format