School of Computing

Exhaustive testing of safety critical java

Tomas Kalibera, Pavel Parizek, Michal Malohlava, and Martin Schoeberl

In Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems (JTRES), pages 182-196. ACM, August 2010 [doi].

Abstract

With traditional testing, the test case has no control over non-deterministic scheduling decisions, and thus errors dependent on scheduling are only found by pure chance. Java Path Finder (JPF) is a specialized Java virtual machine that can systematically explore execution paths for all possible schedulings, and thus catch these errors. Unfortunately, execution-based model checkers, including JPF, cannot be easily adapted to support real-time programs.

We propose a scheduling algorithm for JPF which allows testing of Safety Critical Java (SCJ) applications with periodic event handlers at SCJ levels 0 and 1 (without aperiodic event handlers). The algorithm requires that deadlines are not missed and that there is an execution time model that can give best- and worst-case execution time estimates for a given program path and specific program inputs.

Our implementation, named \toolname, allows to search for scheduling dependent memory access errors, certain invalid argument errors, priority ceiling emulation protocol violations, and failed assertions in application code in SCJ programs for levels 0 and 1. It uses the execution time model of the Java Optimized Processor (JOP). We test our tool with Collision Detector and PapaBench application benchmarks. We provide an SCJ version of the C PapaBench benchmark, which implements an autopilot that has flown real UAVs.

Download publication 218 kbytes (PDF)

Bibtex Record

@inproceedings{3123,
author = {Tomas Kalibera and Pavel Parizek and Michal Malohlava and Martin Schoeberl},
title = {Exhaustive testing of safety critical Java},
month = {August},
year = {2010},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {10.1145/1850771.1850794},
url = {http://www.cs.kent.ac.uk/pubs/2010/3123},
    publication_type = {inproceedings},
    submission_id = {5982_1308764916},
    ISBN = {978-1-4503-0122-0},
    booktitle = {Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems (JTRES)},
    publisher = {ACM},
    refereed = {Yes},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014