Nipkow, Tobias (Prof., Ph.D.); van de Pol, Jaco (Prof. Dr.)
Sprache:
en
Fachgebiet:
DAT Datenverarbeitung, Informatik
TU-Systematik:
DAT 706d; DAT 540d
Kurzfassung:
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. By constructing the checker in Isabelle/HOL, the same level of trustworthiness is achieved.
«
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...
»
Übersetzte Kurzfassung:
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 ihr Ergebnis zu erzeugen. Ein unabhängiger Checker bestätigt, dass das Zertifikat korrekt ist. Durch Konstruktion des Checkers in Isabelle/HOL wird dasselbe Level von Vertrauenswürdigkeit erreicht.
«
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...
»