Maschinelle Verifikation von parametrisierten Echtzeitsystemen
| dc.contributor.author | Göthel, Thomas | |
| dc.contributor.editor | Hölldobler, Steffen | |
| dc.date.accessioned | 2020-08-21T08:45:57Z | |
| dc.date.available | 2020-08-21T08:45:57Z | |
| dc.date.issued | 2013 | |
| dc.description.abstract | 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. | de |
| dc.identifier.isbn | 978-3-88579-417-2 | |
| dc.identifier.pissn | 1617-5468 | |
| dc.identifier.uri | https://dl.gi.de/handle/20.500.12116/33727 | |
| dc.language.iso | de | |
| dc.publisher | Gesellschaft für Informatik | |
| dc.relation.ispartof | Ausgezeichnete Informatikdissertationen 2012 | |
| dc.relation.ispartofseries | Lecture Notes in Informatics (LNI) - Dissertations, Volume D-13 | |
| dc.title | Maschinelle Verifikation von parametrisierten Echtzeitsystemen | de |
| gi.citation.endPage | 130 | |
| gi.citation.publisherPlace | Bonn | |
| gi.citation.startPage | 121 |
Dateien
Originalbündel
1 - 1 von 1
Vorschaubild nicht verfügbar
- Name:
- 121.pdf
- Größe:
- 241.27 KB
- Format:
- Adobe Portable Document Format