SCJ-Circus: specification and refinement of Safety-Critical Java programs
Miyazawa Alvaro Heiji, Cavalcanti Ana Lucia Caneca and Wellings Andrew John
Safety-Critical Java (SCJ) is a version of Java for real-time, embedded, safety-critical applications. It supports certification via abstractions that enforce a particular program architecture, with controlled concurrency and memory models. SCJ is an Open Group standard, with a reference implementation, but little support for reasoning. Here, we present SCJ-Circus, a refinement notation for specification and verification of low-level models of SCJ programs. SCJ-Circus is part of the Circus family of state-rich process algebras: it includes the Circus constructs for modelling of sequential and concurrent behaviour based on Z and CSP, and the real-time and object-oriented extensions of Circus, in addition to the SCJ abstractions. We present the syntax of SCJ-Circus and its semantics, defined by mapping SCJ-Circus constructs to those of Circus. We also detail a refinement strategy that takes a Circus design that adheres to a multiprocessor cyclic executive pattern and produces an SCJ program design, described in SCJ-Circus. Finally, we show how this refinement strategy can be extended for more complex program architectures.
Download Not Available
BibTex Entry
@article{Miyazawa_2019,
author = {Miyazawa, {Alvaro Heiji} and Cavalcanti, {Ana Lucia Caneca} and Wellings, {Andrew John}},
day = {11},
doi = {10.1016/j.scico.2019.01.002},
issn = {0167-6423},
journal = {Science of Computer Programming},
keywords = {SCJ, missions, event handlers, process algebra, semantics, refinement},
language = {English},
month = {1},
note = {{\circledC} 2019 Elsevier B.V. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy.},
pages = {140--176},
publisher = {Elsevier},
pure_url = {https://pure.york.ac.uk/portal/en/publications/scjcircus-specification-and-refinement-of-safetycritical-java-programs(e03a5ae2-7cbb-4e61-abb9-91c483aa1501).html},
title = {SCJ-Circus: specification and refinement of Safety-Critical Java programs},
url = {https://doi.org/10.1016%2Fj.scico.2019.01.002},
volume = {181},
year = {2019}
}