The purpose of this thesis is to create a coupling of the formal specification framework FOCUS in the generic theorem prover Isabelle/HOL, a logical framework based on Higher-Order Logic. The main focus of this work is on specification and verification of embedded real-time systems. The key contributions of the thesis are (1) Deep embedding of that part of the framework FOCUS, which is appropriate for the specification of real-time systems, into Isabelle/HOL. „FOCUS on Isabelle“ enables to validate and verify system specifications in a methodological way. (2) Syntax extensions for FOCUS for the argumentation over time intervals: a special kind of tables, timed state transition diagrams, and a number of new operators. The deep embedding into Isabelle/HOL includes all these extensions. (3) Schemata for automatic correctness proofs in Isabelle/HOL of the syntactic interfaces for specified system components.     «

The purpose of this thesis is to create a coupling of the formal specification framework FOCUS in the generic theorem prover Isabelle/HOL, a logical framework based on Higher-Order Logic. The main focus of this work is on specification and verification of embedded real-time systems. The key contributions of the thesis are (1) Deep embedding of that part of the framework FOCUS, which is appropriate for the specification of real-time systems, into Isabelle/HOL. „FOCUS on Isabelle“ enables to va...     »

Das Ziel dieser Arbeit ist die Realisierung einer Kopplung des formalen Spezifikationssystems FOCUS mit dem generischen Theorembeweiser Isabelle/HOL zur rechnergestützte Verifikation von eingebetteten Echtzeitssystemen. Die zentralen Beiträge der Arbeit sind: (1) Tiefe Einbettung der Teile von FOCUS in Isabelle/HOL, die für die Spezifikation der Echtzeitsysteme angebracht sind. „FOCUS on Isabelle“, das Ergebnis der Kopplung, erlaubt Systemspezifikationen zu validieren und zu verifizieren. (2) FOCUS -Syntaxerweiterungen für die Argumentation über den Zeitintervallen: spezielle Tabellen, gezeitete Zustandsübergangsdiagramme und einige neue Operatoren. Die tiefe Einbettung in Isabelle/HOL umfasst alle diese Erweiterungen. (3) Schemata für automatische Korrektheitsbeweise in Isabelle/HOL von syntaktischen Schnittstellen der spezifizierten Systemkomponenten.     «

Das Ziel dieser Arbeit ist die Realisierung einer Kopplung des formalen Spezifikationssystems FOCUS mit dem generischen Theorembeweiser Isabelle/HOL zur rechnergestützte Verifikation von eingebetteten Echtzeitssystemen. Die zentralen Beiträge der Arbeit sind: (1) Tiefe Einbettung der Teile von FOCUS in Isabelle/HOL, die für die Spezifikation der Echtzeitsysteme angebracht sind. „FOCUS on Isabelle“, das Ergebnis der Kopplung, erlaubt Systemspezifikationen zu validieren und zu verifizieren. (2) F...     »