Take a look at the new version of this page: [ beta version ]. Tell us what you think.

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.

REFERENCES

• 1: Absint ait page. URL: http://www.absint.com/ait/.
• 2: Bound-t tool homepage. URL: http://www.bound-t.com/.
• 3: W. Ahrendt, T. Baar, B. Beckert, R. Bubel, M. Giese, R. Hähnle, W. Menzel, W. Mostowski, A. Roth, S. Schlager, and P. H. Schmitt. The KeY tool. Software and System Modeling, 4:32--54, 2005.
• 4: Bernhard Beckert, A Dynamic Logic for the Formal Verification of Java Card Programs, Revised Papers from the First International Workshop on Java on Smart Cards: Programming and Security, p.6-24, September 14, 2000
• 5: M. Berkelaar. lp_solve (mixed integer linear program solver) ftp site. ftp://ftp.es.ele.tue.nl/pub/lp_solve. Reported to have solved models with up to 30,000 variables and 50,000 constraints. A Java version is available at http://www.cs.sunysb.edu/~ algorith/implement/lpsolve/implements.html.
• 6: G. Bernat. Javelin webpage. URL: http://www-users.cs.york.ac.uk/~bernat/javelin/index.html, Mar. 2000.
• 7: G. Bernat, A. Burns, and A. Wellings. Portable worst case execution time analysis using java byte code. In Proc. 12th EUROMICRO conference on Real-time Systems, June 2000.
• 8: G. Bollela. Real-Time Specification for Java. Addison-Wesley, 2001.
• 9: Object Modeling with the OCL, The Rationale behind the Object Constraint Language, January 2002
• 10: A. Colin. Heptane webpage. URL: http://www.irisa.fr/solidor/work/heptane-demo/heptane.html, Feb. 2001.
• 11: Antoine Colin , Isabelle Puaut, A Modular & Retargetable Framework for Tree-Based WCET Analysis, Proceedings of the 13th Euromicro Conference on Real-Time Systems, p.37, June 13-15, 2001
• 12: Christian Ferdinand , Reinhold Heckmann , Marc Langenbach , Florian Martin , Michael Schmidt , Henrik Theiling , Stephan Thesing , Reinhard Wilhelm, Reliable and Precise WCET Determination for a Real-Life Processor, Proceedings of the First International Workshop on Embedded Software, p.469-485, October 08-10, 2001
• 13: T. Gedell and R. Hähnle. Automating verification of loops by parallelization. submitted, 2006.
• 14: J. Gustafsson, A. Ermedahl, and B. Lisper. Algorithms for infeasible path calculation. In Sixth International Workshop on Worst-Case Execution Time Analysis, (WCET'2006), Dresden, Germany, July 2006.
• 15: David Harel , Jerzy Tiuryn , Dexter Kozen, Dynamic Logic, MIT Press, Cambridge, MA, 2000
• 16: A. Hergenhan , W. Rosenstiel, Static timing analysis of embedded software on advanced processor architectures, Proceedings of the conference on Design, automation and test in Europe, p.552-559, March 27-30, 2000, Paris, France [doi>10.1145/343647.343846]
• 17: A. Hergenhan, A. Siebenborn, and W. Rosenstiel. Studies on different modeling aspects for tight calculations of worst case execution time. In WIP-Proceedings of the 21th IEEE Real-Time Systems Symposium, Orlando FL, USA, Nov. 2000.
• 18: Hija, high-integrity java. www.hija.info, 2004--2006.
• 19: Michael Hind, Pointer analysis: haven't we solved this problem yet?, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.54-61, June 2001, Snowbird, Utah, United States [doi>10.1145/379605.379665]
• 20: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 21: R. Kirner. calc_wcet_167 webpage. URL: http://www.vmars.tuwien.ac.at/~raimund/calc_wcet/, Oct. 2001.
• 22: R. Kirner. The programming language wcetc. Research Report 2/2002, Technische Universität Wien, Institut für Technische Informatik, Treitlstr. 1-3/182-1, 1040 Vienna, Austria, 2002.
• 23: G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. Cok, and J. Kiniry. JML Reference Manual, Nov. 2004. Draft revision 1.98.
• 24: G. T. Levens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. Cok, and J. Kiniry. JML reference manual. http://www.jmlspec.org/, 2004.
• 25: Y.-T. S. Li. Cinderella 3.0 home page. URL: http://www.ee.princeton.edu/~yauli/cinderella-3.0/, Oct. 1996.
• 26: Bertrand Meyer, Applying "Design by Contract", Computer, v.25 n.10, p.40-51, October 1992 [doi>10.1109/2.161279]
• 27: Ana Milanova , Atanas Rountev , Barbara G. Ryder, Parameterized object sensitivity for points-to and side-effect analyses for Java, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy [doi>10.1145/566172.566174]
• 28: Conference Record of the Twenty-first Annual ACM Symposium on Principles of Programming Languages, ACM SIGPLAN Notices. ACM Press, Jan. 1994.
• 29: P. Puschner , Ch. Koza, Calculating the maximum, execution time of real-time programs, Real-Time Systems, v.1 n.2, p.159-176, Sep. 1989 [doi>10.1007/BF00571421]
• 30: M. Tofte. A brief introduction to Regions. pages 186--195, 1998.
• 31: Mads Tofte , Jean-Pierre Talpin, Region-based memory management, Information and Computation, v.132 n.2, p.109-176, Feb. 1, 1997 [doi>10.1006/inco.1996.2613]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Algorithms, Performance, Reliability, Theory, Verification

Keywords:
data flow, deductive verification, formal analysis, realtime java, worst case execution time, worst case memory usage