Provably Correct Loops Bounds for Realtime Java Programs

James J. Hunt, Fridtjof B. Siebert, Peter H. Schmitt, Isabel Tonin


13 Oct 2006
JTRES'06 - The 4th International Workshop on Java Technologies for Real-time and Embedded Systems - Paris, France



Determining concrete bounds for loops is one of the more vexing problems of resource analysis of realtime programs. Current mechanisms are limited in scope and require considerable user input that can not be verified. The authors present a methodology for providing more general loop bounds where the correctness can be demonstrated with formal techniques. The methodology combines data flow analysis and deductive formal verification to attain this goal.

Download: PDF icon PDF (133kB)