KIT | KIT-Bibliothek | Impressum
Open Access Logo
§
Volltext
URN: urn:nbn:de:swb:90-140874

Deductive Verification of Safety-Critical Java Programs

Engel, Christian

Abstract:
This work investigates the application of deductive verification techniques to safety critical Java programs, in particular RTSJ programs. A focus is put on the formalization of the RTSJ memory model in dynamic logic, the utilization of a region-based memory model for ensuring non-interference and a design-by-contract based approach for the formal specification and verification of worst case memory consumption.


Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Jahr 2009
Sprache Englisch
Identifikator URN: urn:nbn:de:swb:90-140874
KITopen ID: 1000014087
Verlag Karlsruhe
Abschlussart Dissertation
Fakultät Fakultät für Informatik (INFORMATIK)
Institut Institut für Theoretische Informatik (ITI)
Prüfungsdaten 13.11.2009
Referent/Betreuer Prof. P. Schmitt
Schlagworte Formal Methods, Verification, Real-Time, Formal Specification, Java
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page