Safety-critical Java programs from Circus models

Safety-Critical Java (SCJ) is a novel version of Java that addresses issues related to real-time programming and certification of safety-critical applications. In this paper, we propose a technique that reveals the issues involved in the formal verification of an SCJ program, and provides guidelines for tackling them in a refinement-based approach. It is based on Circus, a combination of well established notations: Z, CSP, Timed CSP, and object orientation. We cater for the specification of timing requirements and their decomposition towards the structure of missions and event handlers of SCJ. We also consider the integrated refinement of value-based specifications into class-based designs using SCJ scoped memory areas. We present a refinement strategy, a Circus variant that captures the essence of the SCJ paradigm, and a substantial example based approach on a concurrent version of a case study that has been used as a benchmark by the SCJ community: an aircraft collision detector.