Refining SCJ Mission Specifications into Parallel Handler Designs

Frank Zeyda
(University of York)
Ana Cavalcanti
(University of York)

Safety-Critical Java (SCJ) is a recent technology that restricts the execution and memory model of Java in such a way that applications can be statically analysed and certified for their real-time properties and safe use of memory. Our interest is in the development of comprehensive and sound techniques for the formal specification, refinement, design, and implementation of SCJ programs, using a correct-by-construction approach. As part of this work, we present here an account of laws and patterns that are of general use for the refinement of SCJ mission specifications into designs of parallel handlers used in the SCJ programming paradigm. Our notation is a combination of languages from the Circus family, supporting state-rich reactive models with the addition of class objects and real-time properties. Our work is a first step to elicit laws of programming for SCJ and fits into a refinement strategy that we have developed previously to derive SCJ programs.

In John Derrick, Eerke Boiten and Steve Reeves: Proceedings 16th International Refinement Workshop (Refine 2013), Turku, Finland, 11th June 2013, Electronic Proceedings in Theoretical Computer Science 115, pp. 52–67.
Published: 24th May 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: