Deductive Verification of RTSJ Programs

The Real-Time Specification for Java (RTSJ) defines a region-based memory model with the capability to ex-plicitely free memory regions (so called scoped memory ar-eas). For preventing dangling references it introduces run-time checks, raising errors in the case of a failure, to re-strict the creation of references between objects residing in different regions. This work presents how an existing dy-namic logic calculus for Java is extended to handle RTSJ’s memory model, thus enabling to prove the absence of failed runtime checks. This is crucial for giving safety guarantees for RTSJ applications or could allow the Java Virtual Ma-chine (JVM) to skip these kind of runtime checks resulting in improved performance