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...     »

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...     »