The safety-critical java memory model: A formal account

Abstract

Safety-Critical Java (SCJ) is a version of Java for real-time programming that facilitates certification of implementations of safety-critical systems. It is the result of an international effort involving industry and academia. What we provide here is, as far as we know, the first formalisation of the SCJ model of memory regions. We use the Unifying Theories of Programming (UTP) to enable the integration of our theory with refinement models for object-orientation and concurrency. In developing the SCJ theory, we also make a contribution to the UTP by providing a general theory of invariants (of which the SCJ theory is an instance). Our results are a first essential ingredient to formalise the novel programming paradigm embedded in SCJ, and enable the justification and development of reasoning techniques based on refinement. © 2011 Springer-Verlag.