Provably correct loops bounds for realtime Java programs

Abstract

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.