Exhaustive testing of safety critical Java

Kalibera, Tomas and Parizek, Pavel and Malohlava, Michal and Schoeberl, Martin (2010) Exhaustive testing of safety critical Java. In: Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems (JTRES). (doi:https://doi.org/10.1145/1850771.1850794) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided. (Contact us about this Publication)
Official URL


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.

Item Type: Conference or workshop item (UNSPECIFIED)
Uncontrolled keywords: determinacy analysis, Craig interpolants
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing
Depositing User: T. Kalibera
Date Deposited: 21 Sep 2012 09:49 UTC
Last Modified: 21 Sep 2012 09:49 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/30643 (The current URI for this page, for reference purposes)
  • Depositors only (login required):