Logic and Formal Methods

Deductive Verification of Safety-Critical Java Programs

  • Author(s):

    Christian Engel

  • 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.