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

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.

• Publication year

  2016

• Venue

  Refine@FM

• Publication date

  2016-06-07

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.4204/EPTCS.209.6arXiv 1606.02021
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Refinement-based verification of implementations of Stateflow charts

  2014cited by this paper
• Circus Models for Safety-Critical Java Programs

  2014influential reference
• SCJ: Memory-Safety Checking without Annotations

  2014cited by this paper
• Safety-critical Java programs from Circus models

  2013influential reference
• Unifying Theories of Programming

  2012cited by this paper
• Formal verification of implementations of Stateflow charts

  2012cited by this paper
• Circus Time with Reactive Designs

  2012cited by this paper
• Refinement-oriented models of Stateflow charts

  2012cited by this paper
• Static checking of safety critical Java annotations

  2010cited by this paper
• The design of SafeJML, a specification language for SCJ with support for WCET specification

  2010cited by this paper
• Understanding Concurrent Systems

  2010cited by this paper
• Exhaustive testing of safety critical Java

  2010cited by this paper
• Control Law Diagrams in Circus

  2005cited by this paper
• Formal derivation of state-rich reactive programs using Circus

  2005influential reference
• Unifying classes and processes

  2005cited by this paper
• Concurrent and real-time programming in Java

  2004cited by this paper
• A Refinement Strategy for Circus

  2003cited by this paper
• An overview of JML tools and applications

  2003cited by this paper
• Using Z - specification, refinement, and proof

  1996cited by this paper

• SCJ-Circus: Specification and refinement of Safety-Critical Java programs

  2019cites this paper
• A strategy to verify the code generation from concurrent and state-rich circus specifications to executable code

  2018cites this paper
• A Sound Operational Semantics for Circus

  2017cites this paper
• Safety-Critical Java Level 2: applications, modelling, and verification

  2016cites this paper
• Orchestration Combinators in Apla+ Language

  2016cites this paper
• Formal analysis of confidentiality conditions related to data leakage

  2016cites this paper
• Formal Methods: Foundations and Applications

  2015cites this paper
• Refinement Strategies for Safety-Critical Java

  2015cites this paper