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 system, and a complex resource contention example involving autonomous vehicles crossing an intersection. The utility of JPF in finding logic and timing errors is illustrated, and the remaining challenges in supporting all of RTSJ are assessed.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Birtwistle, G.M., Dahl, O.-J., Myhrhaug, B., Nygaard, K.: Simula BEGIN. Auerbach/Studentliteratur, Philadelphia (1973)
Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Optimal scheduling using priced timed automata. ACM SIGMETRICS Performance Evaluation Review 32(4), 34–40 (2005)
Burns, A: The Ravenscar profile, http://polaris.dit.upm.es/~ork/documents/RP_spec.pdf
Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
Corsaro, A., Schmidt, D.C.: Evaluating Real-Time Java features and performance for real-time embedded systems. In: Proc. 8th Real-Time and Embedded Technology and Applications Symposium, September 24-27. IEEE Computer Society, Los Alamitos (2002)
Degani, A.: Taming HAL: Designing Interfaces Beyond 2001. Palgrave Macmillan, Basingstoke (2004)
Dwyer, M.B., Hatcliff, J., Hoosier, M., Robby: Building your own model checker using the Bogor extensible model checking framework. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 148–152. Springer, Heidelberg (2005)
The Real-Time for JavaTM Expert Group, https://rtsj.dev.java.net
Groce, A., Visser, W.: Heuristics for model checking Java programs. International Journal on Software Tools for Technology Transfer (2004)
Havelund, K.: Eagle Flier, a rule-based runtime verification framework, http://yangtze.cs.uiuc.edu/~ksen/eagle/
Jacobs, B., Marche, C., Rauch, N.: Formal verification of a commercial smart card applet with multiple tools. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 241–257. Springer, Heidelberg (2004)
MJI – the Model Java Interface, http://ase.arc.nasa.gov/jpf/MJI.html
Kim, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a run-time assurance tool for Java. In: First International Workshop on Run-time Verification, Paris, France. Electronic Notes in Theoretical Computer Science, vol. 55 (2), July 23 (2001)
Lindstrom, G.: RTSJ-JPF API, http://www.cs.utah.edu/~gary/RTSJ/doc/
Douglass Locke, C.: Real-Time Java moving into the mainstream. RTC Journal (January 2004)
Parareanu, C.S., Khurshid, S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553–568. Springer, Heidelberg (2003)
Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Automated Software Engineering Journal 10(2) (April 2003)
Visser, W., Pasareanu, C.S., Khurshid, S.: Test input generation with Java PathFinder. In: Proceedings of ISSTA (July 2004)
Wellings, A.: Concurrent and Real-Time Programming in Java. John Wiley & Sons, Ltd., Chichester (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lindstrom, G., Mehlitz, P.C., Visser, W. (2005). Model Checking Real Time Java Using Java PathFinder. In: Peled, D.A., Tsay, YK. (eds) Automated Technology for Verification and Analysis. ATVA 2005. Lecture Notes in Computer Science, vol 3707. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562948_33
Download citation
DOI: https://doi.org/10.1007/11562948_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29209-8
Online ISBN: 978-3-540-31969-6
eBook Packages: Computer ScienceComputer Science (R0)