Publications

Click on the titles to view and download the abtracts.

A case study of specification and verification using JML in an avionics application

Published/Presented at: 
JTRES'06 - The 4th International Workshop on Java Technologies for Real-time and Embedded Systems, Paris, France
Author: 
James J. Hunt, Peter Schmitt, Isabel Tonin, Claus Wonnemann, Eric Jenn, Stéphane Leriche

The literature for deductive formal verification is quite rich; however, very few case studies have been done. The authors present a case study of using deductive formal verification of a navigation system from the avionics domain. Both writing the specifications and their verification with a runtime assertion checker and KEY, a tool using automatic theorem proving techniques for verifying JAVA programs, are covered.

Issues in building an ANRTS platform

Published/Presented at: 
JTRES'06 - The 4th International Workshop on Java Technologies for Real-time and Embedded Systems, Paris, France
Author: 
Antonio Kung, James J. Hunt, Ludovic Gauthier, Marc Richard-Foy

The HIJA initiative is currently working on creating the technology conditions to achieve architecture neutrality for real-time systems. To this end it has developed a number of profiles based on RTSJ and developed a number of proofs of concept. In doing so, HIJA came across a number of integration issues which are not specific to the chosen technologies, and therefore need to be addressed by the embedded systems technology community in the large.

HIJA Proposal for Safety Critical Java

Published/Presented at: 
Version 0.5, Draft
Author: 
aicas

Executive Summary

This document contains the current HIJA proposal for safety critical Java. It should not be seen as a single proposal; rather it is a series of proposals for various aspects of a safety critical java standard. It is organized along similar lines as the Real-Time Specification for Java. The appendix contains some optional standard features.

Proposal Overview

Analysis Tools for the HIJA Safety-Critical Java Model

Published/Presented at: 
DASIA'05 - Data Systems In Aerospace - Edinburgh, Scotland.
Author: 
Fridtjof Siebert

The European project HIJA (High-Integrity Java) started its work on defining and implementing a new High-Integrity Java for future networked real-time embedded systems in June 2004. Based on the features of the Realtime Specification for Java (RTSJ), a safety-critical profile is defined. This profile provides a restricted subset with the aim to permit certification up the DO178B level A.

Improving Software Quality in Safety-Critical Applications by Model-Driven Verification

Published/Presented at: 
ENTCS Vol. 133 May 2005 - Electronic Notes in Theoretical Computer Science (ENTCS) Volume 133, May, 2005
Author: 
Dr. James J. Hunt, Anders Henriksson, Uwe Aßman

We propose a new development scheme for quality-aware applications, quality-driven development (QDD), based on the Model-Driven Architecture (MDA) of Object Management Group OMG. We argue that software development in areas, such as real-time systems, should not only rely on code verification, but also on design verification, and show that a slightly extended MDA process offers the opportunity to integrate system development together with design verification. As an instance of the method, we present the MDA-based tool environment of the HIDOORS project [Karlsruhe James Hunt.

The Impact of Realtime Garbage Collection on Realtime Java Programming

Published/Presented at: 
ISORC'04 - The 7th IEEE International Symposium on Object-oriented Real-time distributed Computing - Vienna, Austria
Author: 
Fridtjof Siebert

Extensions like the Real-Time Specification for Java (RTSJ) enable the use of Java in more and more time-critical application domains. The RTSJ enables the development of realtime code in Java even though a classical garbage collector causes unpredictable pauses to non-realtime code.

Pages