Safety-critical Java programs from Circus models

Research output: Contribution to journalArticlepeer-review


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.
Original languageEnglish
Pages (from-to)614-667
Number of pages54
JournalReal-Time Systems
Issue number5
Early online date10 May 2013
Publication statusPublished - Sept 2013


  • SCJ
  • Circus
  • RTSJ
  • Real-time systems
  • Refinement
  • Verification

Cite this