SCJ-Circus: a refinement-oriented formal notation for Safety-Critical Java

Alvaro Miyazawa
(University of York)
Ana Cavalcanti
(University of York)

Safety-Critical Java (SCJ) is a version of Java whose goal is to support the development of real-time, embedded, safety-critical software. In particular, SCJ supports certification of such software by introducing abstractions that enforce a simpler architecture, and simpler concurrency and memory models. In this paper, we present SCJ-Circus, a refinement-oriented formal notation that supports the specification and verification of low-level programming models that include the new abstractions introduced by SCJ. SCJ-Circus is part of the family of state-rich process algebra Circus, as such, SCJ-Circus includes the Circus constructs for modelling sequential and concurrent behaviour, real-time and object orientation. We present here the syntax and semantics of SCJ-Circus, which is defined by mapping SCJ-Circus constructs to those of standard Circus. This is based on an existing approach for modelling SCJ programs. We also extend an existing Circus-based refinement strategy that targets SCJ programs to account for the generation of SCJ-Circus models close to implementations in SCJ.

In John Derrick, Eerke Boiten and Steve Reeves: Proceedings 17th International Workshop on Refinement (Refine'15), Oslo, Norway, 22nd June 2015, Electronic Proceedings in Theoretical Computer Science 209, pp. 71–86.
Published: 4th June 2016.

ArXived at: https://dx.doi.org/10.4204/EPTCS.209.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org