The RTEmbed extension for Java Pathfinder is aimed at verification of Java programs for real-time and embedded platforms, such as RTSJ and SCJ.
Features
Currently, the extension includes the following components:
- implementation of a significant part of RTSJ API and its semantics (e.g., region-based memory model),
- implementation of a significant part of SCJ API and its semantics (levels 0 and 1 are supported),
- RTSJ-compliant scheduler based on thread priorities, periods and releases, and limited preemption,
- abstraction of real time clock based on thread periods and numbers of past thread releases,
- thread scheduling for SCJ and model of time based on WCET for bytecode instructions on the JOP processor (http://www.jopdesign.com),
- a listener that detects invalid usage of scoped memory areas (including private and mission memory areas in SCJ), and
- a general optimization of state space traversal based on platform-specific restrictions of concurrency.
Related publications
- Pavel Parizek and Tomas Kalibera. Platform-Specific Restrictions on Concurrency in Model Checking of Java Programs, In Proceedings of the 14th International Workshop on Formal Methods for Industrial Critical Systems (FMICS), LNCS, vol. 5825, 2009. pdf
- Tomas Kalibera, Pavel Parizek, Michal Malohlava, and Martin Schoeberl. Exhaustive Testing of Safety Critical Java, In Proceedings of the 8th International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES 2010), ACM, 2010. pdf