By the same authors

From the same journal

From the same journal

The Safety-Critical Java Memory Model Formalised

Research output: Contribution to journalArticlepeer-review

Author(s)

Department/unit(s)

Publication details

JournalFormal Aspects of Computing
DatePublished - Jan 2013
Issue number1
Volume25
Number of pages21
Pages (from-to)37-57
Original languageEnglish

Abstract

Safety-Critical Java (SCJ) is a version of Java for real-time programming, restricted to facilitate certification of implementations of safety-critical systems. Its development is the result of an international effort involving experts from industry and academia. What we provide here is, as far as we know, the first formalisation of the SCJ model of memory regions. We use Hoare and He’s unifying theories of programming (UTP), enabling the integration of our theory with refinement models for object orientation and concurrency. In developing the SCJ theory, we also make a contribution to UTP by providing a general theory of invariants (an instance of which is used in the SCJ theory). The results presented here are a first essential ingredient to formalise the novel programming paradigm embedded in SCJ, and enable the justification and development of formal reasoning techniques based on refinement.

    Research areas

  • Safety-Critical Java; Memory safety; Semantics; Unifying theories of programming; Integration; Refinement

Research outputs

Projects

Discover related content

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

View graph of relations