By the same authors

From the same journal

From the same journal

Safety-critical Java programs from Circus models

Research output: Contribution to journalArticle



Publication details

JournalReal-Time Systems
DateE-pub ahead of print - 10 May 2013
DatePublished (current) - Sep 2013
Issue number5
Number of pages54
Pages (from-to)614-667
Early online date10/05/13
Original languageEnglish


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.

    Research areas

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

Research outputs


Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations