Modelling and verifying a priority scheduler for an SCJ runtime environment

Freitas, L; Baxter, J; Calvacanti, A; Wellings, A

doi:10.1007/978-3-319-33693-0_5

Modelling and verifying a priority scheduler for an SCJ runtime environment

Lookup NU author(s): Dr Leo Freitas

Downloads

Published version [.pdf]

Licence

This work is licensed under a Creative Commons Attribution 4.0 International License (CC BY 4.0).

Abstract

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.