User: Guest  Login
Original title:
Trustworthy Verification of Realtime Systems 
Translated title:
Vertrauenswürdige Verifikation von Echtzeitsystemen 
Year:
2020 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Nipkow, Tobias (Prof., Ph.D.) 
Referee:
Nipkow, Tobias (Prof., Ph.D.); van de Pol, Jaco (Prof. Dr.) 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
TUM classification:
DAT 706d; DAT 540d 
Abstract:
Timed automata are a popular formalism for modeling real-time systems. Model checkers for timed automata can automatically prove the safety of such a model. This thesis addresses the question of the trustworthiness of these tools. In a first approach, a model checker for timed automata was constructed within the highly trustworthy theorem prover Isabelle/HOL. Next, unverified model checkers were modified to produce a proof for their result. An independent checker confirms that the proof is valid...    »
 
Translated abstract:
Timed Automata sind ein beliebter Formalismus, um Echtzeitsysteme zu modellieren. Model-Checker für Timed Automata können automatisch die Sicherheit eines solchen Modells beweisen. Diese Dissertation nimmt sich der Frage der Vertrauenswürdigkeit dieser Werkzeuge an. In einem ersten Ansatz wurde ein Model-Checker für Timed Automata innerhalb des höchst vertrauenswürdigen Theorembeweisers Isabelle/HOL konstruiert. Anschließend wurden unverifizierte Model-Checker modifiziert, um einen Beweis für ih...    »
 
Oral examination:
09.12.2020 
File size:
11754842 bytes 
Pages:
177 
Last change:
23.02.2021