Analysis Tools for the HIJA Safety-Critical Java Model
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.
The aspects covered by the profile address the supported thread model, synchronization mechanism, memory model and annotations that permit tools to perform correctness verification. In parallel, formal verification tools are developed to proof the functional and non-functional (resource use, etc.) correctness of an application.
Download: PDF (133k)