Lookup NU author(s): Dr Leo Freitas
This work is licensed under a Creative Commons Attribution 4.0 International License (CC BY 4.0).
Safety-Critical Java (SCJ) is a version of Java suitable for programming real-time safety-critical systems; it is the result of an international standardisation eort to dene a subset of the Real-Time Specication for Java (RTSJ). SCJ programs require the use of specialised virtual machines. We present here the result of our verication of the scheduler of the only SCJ virtual machine up to date with the standard and publicly available, the icecap HVM. We describe our approach for analysis of (SCJ) virtual machines, and illustrate it using the icecap HVM scheduler. Our work is based on a state-rich process algebra that combines Z and CSP, and we take advantage of well established tools.
Author(s): Freitas L, Baxter J, Calvacanti A, Wellings A
Publication type: Conference Proceedings (inc. Abstract)
Publication status: Published
Conference Name: Integrated Formal Methods: 12th International Conference (iFM 2016)
Year of Conference: 2016
Online publication date: 24/05/2016
Acceptance date: 02/04/2016
Date deposited: 18/03/2016
Library holdings: Search Newcastle University Library for this item
Series Title: Lecture Notes in Computer Science