SCJ-Circus: specification and refinement of Safety-Critical Java programs

TY - JOUR

T1 - SCJ-Circus: specification and refinement of Safety-Critical Java programs

AU - Miyazawa, Alvaro Heiji

AU - Cavalcanti, Ana Lucia Caneca

AU - Wellings, Andrew John

N1 - © 2019 Elsevier B.V. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy.

PY - 2019/7/15

Y1 - 2019/7/15

N2 - 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.

AB - 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.

KW - SCJ

KW - missions

KW - event handlers

KW - process algebra

KW - semantics

KW - refinement

UR - http://www.scopus.com/inward/record.url?scp=85060444150&partnerID=8YFLogxK

U2 - 10.1016/j.scico.2019.01.002

DO - 10.1016/j.scico.2019.01.002

M3 - Article

SN - 0167-6423

VL - 181

SP - 140

EP - 176

JO - Science of Computer Programming

JF - Science of Computer Programming

ER -