Java in the Safety-Critical Domain
Cavalcanti, Ana and Miyazawa, Alvaro and Wellings, Andy and Woodcock, Jim and Zhao, Shuai
Safety-Critical Java (SCJ) is an Open Group standard that defines a novel version of Java suitable for programming systems with various levels of criticality. SCJ enables real-time programming and certification of safety-critical applications. This tutorial presents SCJ and an associated verification technique to prove correctness of programs based on refinement. For modelling, we use the family of notations, which combine Z, CSP, Timed CSP, and object orientation. The technique caters for the specification of functional and timing requirements, and establishes the correctness of designs based on architectures that use the structure of missions and event handlers of SCJ. It also considers the integrated refinement of value-based specifications into class-based designs using SCJ scoped memory areas. As an example, we use an SCJ implementation of a widely used leadership-election protocol.
Download Not Available
BibTex Entry
@inbook{Cavalcanti2017,
address = {Cham},
author = {Cavalcanti, Ana
and Miyazawa, Alvaro
and Wellings, Andy
and Woodcock, Jim
and Zhao, Shuai},
booktitle = {Engineering Trustworthy Software Systems: Second International School, SETSS 2016, Chongqing, China, March 28 - April 2, 2016, Tutorial Lectures},
doi = {10.1007/978-3-319-56841-6_4},
editor = {Bowen, Jonathan P.
and Liu, Zhiming
and Zhang, Zili},
isbn = {978-3-319-56841-6},
pages = {110--150},
publisher = {Springer International Publishing},
title = {Java in the Safety-Critical Domain},
year = {2017}
}