The Real-Time Specification for Java (RTSJ) features a region-based memory model with the capability to explicitly free memory regions (so called scoped memory areas). For preventing dangling references it introduces runtime checks, raising errors in the case of a failure, to restrict the creation of references between objects residing in different regions. This work presents an operational semantics for the RTSJ memory model formulated in a sequent calculus for dynamic logic. The calculus employs symbolic execution and can be used for proving the absence of failed runtime checks. This is crucial for giving safety guarantees for RTSJ applications or could allow an RTSJ compliant Java Virtual Machine (JVM) to skip this kind of runtime checks resulting in improved performance. The presented approach has been implemented in the KeY system and evaluated for its practical feasibility.
A Formalization of the RTSJ Scoped Memory Model in Dynamic Logic