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).
|The full text of this publication is not available from this repository. (Contact us about this Publication)|
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 > Science Technology and Medical Studies > School of Computing|
|Depositing User:||Tomas Kalibera|
|Date Deposited:||21 Sep 2012 09:49|
|Last Modified:||21 Sep 2012 09:49|
|Resource URI:||http://kar.kent.ac.uk/id/eprint/30643 (The current URI for this page, for reference purposes)|
- Depositors only (login required):