Sciweavers

Share
ATVA
2005
Springer

Model Checking Real Time Java Using Java PathFinder

9 years 7 months ago
Model Checking Real Time Java Using Java PathFinder
Abstract. The Real Time Specification for Java (RTSJ) is an augmentation of Java for real time applications of various degrees of hardness. The central features of RTSJ are real time threads; user defined schedulers; asynchronous events, handlers, and control transfers; a priority inheritance based default scheduler; non-heap memory areas such as immortal and scoped, and non-heap real time threads whose execution is not impeded by garbage collection. The Robust Software Systems group at NASA Ames Research Center has Java PathFinder (JPF) under development, a Java model checker. JPF at its core is a state exploring JVM which can examine alternative paths in a Java program (e.g., via backtracking) by trying all nondeterministic choices, including thread scheduling order. This paper describes our implementation of an RTSJ profile (subset) in JPF, including requirements, design decisions, and current implementation status. Two examples are analyzed: jobs on a multiprogramming operating ...
Gary Lindstrom, Peter C. Mehlitz, Willem Visser
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where ATVA
Authors Gary Lindstrom, Peter C. Mehlitz, Willem Visser
Comments (0)
books