The Safety-Critical Java Memory Model Formalised

TY - JOUR

T1 - The Safety-Critical Java Memory Model Formalised

AU - Cavalcanti, Ana Lucia Caneca

AU - Wellings, Andy

AU - Woodcock, Jim

PY - 2013/1

Y1 - 2013/1

N2 - Safety-Critical Java (SCJ) is a version of Java for real-time programming, restricted to facilitate certification of implementations of safety-critical systems. Its development is the result of an international effort involving experts from 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 Hoare and He’s unifying theories of programming (UTP), enabling the integration of our theory with refinement models for object orientation and concurrency. In developing the SCJ theory, we also make a contribution to UTP by providing a general theory of invariants (an instance of which is used in the SCJ theory). The results presented here are a first essential ingredient to formalise the novel programming paradigm embedded in SCJ, and enable the justification and development of formal reasoning techniques based on refinement.

AB - Safety-Critical Java (SCJ) is a version of Java for real-time programming, restricted to facilitate certification of implementations of safety-critical systems. Its development is the result of an international effort involving experts from 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 Hoare and He’s unifying theories of programming (UTP), enabling the integration of our theory with refinement models for object orientation and concurrency. In developing the SCJ theory, we also make a contribution to UTP by providing a general theory of invariants (an instance of which is used in the SCJ theory). The results presented here are a first essential ingredient to formalise the novel programming paradigm embedded in SCJ, and enable the justification and development of formal reasoning techniques based on refinement.

KW - Safety-Critical Java; Memory safety; Semantics; Unifying theories of programming; Integration; Refinement

UR - http://www.scopus.com/inward/record.url?scp=84862737830&partnerID=8YFLogxK

U2 - 10.1007/s00165-012-0253-4

DO - 10.1007/s00165-012-0253-4

M3 - Article

SN - 0934-5043

VL - 25

SP - 37

EP - 57

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 1

ER -