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.
Deductive Verification of Safety-Critical Java Programs
| Author(s): | Links: | Links_bearbeiten | |
|---|---|---|---|
| Source: | |||
| Date: | 2009 | ||
