Deductive Verification of RTSJ Programs
2nd Junior Researcher Workshop on Real-Time Computing (JRWRTC 2008), Rennes, France, 2008
The Real-Time Specification for Java (RTSJ) defines a region-based memory model with the capability to explicitely 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 how an existing dynamic 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 Machine (JVM) to skip these kind of runtime checks resulting in improved performance.