Benutzer: Gast  Login
Originaltitel:
Specification and Seamless Verification of Embedded Real-Time Systems: FOCUS on Isabelle 
Übersetzter Titel:
Spezifikation und Verifikation eingebetteter Echtzeitsysteme: FOCUS on Isabelle 
Jahr:
2007 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Broy, Manfred (Prof. Dr. Dr. h.c.) 
Gutachter:
Nipkow, Tobias (Prof., Ph.D.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Stichworte:
Specification, Verification, Embedded Real-Time Systems, Theorem Proving, Isabelle, FOCUS 
Übersetzte Stichworte:
Spezifikation, Verifikation, Eingebettete Echtzeitsysteme, Isabelle, FOCUS, Maschinengestütztes Beweisen 
Schlagworte (SWD):
Echtzeitsystem; Eingebettetes System; Softwarespezifikation; Verifikation 
TU-Systematik:
DAT 263d; DAT 335d; DAT 325d 
Kurzfassung:
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 v...    »
 
Übersetzte Kurzfassung:
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...    »
 
Mündliche Prüfung:
18.10.2007 
Seiten:
287 
Letzte Änderung:
24.09.2008