Home | deutsch  | Legals | Sitemap | KIT

Deductive Verification of Safety-Critical Java Programs

Deductive Verification of Safety-Critical Java Programs
Author(s):

Christian Engel

Links:
Source:

Digitales Volltextarchiv des KIT

Date: 2009

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.