Titel: An online model-checking framework for timed automata
Sprache: English (United States)
Autor/Autorin: Rinast, Jonas 
Schlagwörter: Formal Methods;Model Checking;Online Model Checking;State Space Reconstruction;Cyber-Physical Systems
Erscheinungsdatum: 2015
Zusammenfassung (deutsch): Diese Dissertation untersucht Online Model Checking, eine dynamische Variante von Model Checking, die Eigenschaften eines Modells analysieren kann, auch wenn längerfristig korrekte Modelle nicht verfügbar sind. Ein Framework, das einen ganzheitlichen Ansatz zur Erstellung solcher Online Model-Checking Anwendungen mit Datenverarbeitungs-, Simulations-, Verifikations- und Visualisierungskomponenten bereitstellt wird präsentiert. Die Korrektheit zweier verwendeter Transformationsreduktionen wird gezeigt. Weiterhin werden zwei Studien zu Online Model Checking im medizinischen Bereich präsentiert.
Zusammenfassung (englisch): This dissertation explores online model checking, a dynamic variant of model checking, that can be used to prove properties of a system even if long-term models for the system are not available. A framework is presented that provides an integrated approach to creating such online model-checking applications with data acquisition, data processing, model simulation, model verification, and simulation visualization features. The correctness of two transformation reductions used is shown. Furthermore, two case studies on online model checking in the medical domain are presented.
URI: http://tubdok.tub.tuhh.de/handle/11420/1256
DOI: 10.15480/882.1253
Institut: Softwaresysteme E-16 
Dokumenttyp: Dissertation
Hauptberichter: Schupp, Sibylle 
Gradverleihende Einrichtung: Technische Universität Hamburg
Enthalten in den Sammlungen:tub.dok

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
OnlineModelCheckingFramework.pdf3,1 MBAdobe PDFMiniaturbild
Öffnen/Anzeigen
Zur Langanzeige

Seitenansichten

334
Letzte Woche
1
Letzten Monat
5
checked on 22.09.2018

Download(s)

504
checked on 22.09.2018

Google ScholarTM

Prüfe


Diese Ressource wurde unter folgender Copyright-Bestimmung veröffentlicht: Lizenz von Creative Commons Creative Commons