By the same authors

From the same journal

From the same journal

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

Research output: Contribution to journalArticle

Published copy (DOI)

Author(s)

Department/unit(s)

Publication details

JournalScience of Computer Programming
DateAccepted/In press - 6 Jan 2019
DateE-pub ahead of print (current) - 11 Jan 2019
Number of pages45
Early online date11/01/19
Original languageEnglish

Abstract

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.

Bibliographical note

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

    Research areas

  • SCJ, missions, event handlers, process algebra, semantics, refinement

Discover related content

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

View graph of relations