Logik und Formale Methoden

Deductive Verification of Safety-Critical Java Programs

  • Autor(en):

    Christian Engel

  • Quelle:

    Digitales Volltextarchiv des KIT

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