Proving the absence of RTSJ related runtime errors through data flow analysis

ABSTRACT

The Real-Time Specification for Java (RTSJ) introduces region based memory management to avoid the need for garbage collection. This region based memory management, however, introduces new possible runtime errors. Ensuring that an RTSJ application executes correctly requires proving that no memory related runtime excpetions can occur.The use of program-wide pointer analysis for proving the absence of runtime error conditions such as null pointer uses or illegal casts is still not widespread. Current uses of program-wide pointer analysis focus on extracting information for optimisations in compilers. In this case, imprecise analysis results only in less agressive optimisation, which is often tolerable.This papers presents the application of a program-wide data flow analysis to prove the absence of memory related runtime errors such as those introduced by the RTSJ.

REFERENCES

• 1: RTCA/DO-178B Software Considerations in Airborne Systems and Equipment Certification, 1992.
• 2: AERO-VM, the hard realtime virtual machine for onboard space systems. www.aero-vm.com, 2003.
• 3: W. Ahrend, T. Baar, B. Becker, R. Bubel, M. Giese, R. Hähnle, W. Menel, W. Mostowski, A. Roth, S. Schlager, and P. H. Schmitt. The Key tool. Technical Report 2003-05, Department of Computer Science, Chalmers University of Technology and Göteborg University (2003), 2002.
• 4: B. Alpern , M. N. Wegman , F. K. Zadeck, Detecting equality of variables in programs, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-11, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73561]
• 5: L. Andersen. Program Analysis and Specialization for the C Programming language. PhD thesis, DIKU, University of Copenhagen, 1994.
• 6: Chris Andreae, James Noble, Yvonne Coady, Celina Gibbs, Jan Vitek, and Tian Zhao. Stars: Scoped types and aspects for real-time systems. In Proceedings of 20th European Conference on Object-Oriented Programming, ECOOP 2006, 2006.
• 7: Marc Berndl , Ondrej Lhoták , Feng Qian , Laurie Hendren , Navindra Umanee, Points-to analysis using BDDs, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 8: Bruno Blanchet , Patrick Cousot , Radhia Cousot , Jérome Feret , Laurent Mauborgne , Antoine Miné , David Monniaux , Xavier Rival, A static analyzer for large safety-critical software, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 9: Greg Bollela. Real-Time Specification for Java. Addison-Wesley, 2001.
• 10: Chandrasekhar Boyapati , Alexandru Salcianu , William Beebee, Jr. , Martin Rinard, Ownership types for safe region-based memory management in real-time Java, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 11: Alan Burns , Brian Dobbing , G. Romanski, The Ravenscar Tasking Profile for High Integrity Real-Time Programs, Proceedings of the 1998 Ada-Europe International Conference on Reliable Software Technologies, p.263-275, June 08-12, 1998
• 12: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, Polymorphic versus Monomorphic Flow-Insensitive Points-to Analysis for C, Proceedings of the 7th International Symposium on Static Analysis, p.175-198, June 29-July 01, 2000
• 13: Manuel Fähndrich , Jakob Rehof , Manuvir Das, Scalable context-sensitive flow analysis using instantiation constraints, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.253-263, June 18-21, 2000, Vancouver, British Columbia, Canada
• 14: D. Garbervetsky G. Salagnac, S. Yovine. Fast escape analysis for region-base memory management. In Proceedings of the 1st Int. Workshop on Abstract Interpretation for Object-Oriented Languages (AIOOL'05), jan 2005.
• 15: HIDOORS, High Integrity Object-Oriented Realtime Systems. www.hidoors.org, 2002--2004.
• 16: HIJA, High-Integrity Java. www.hija.info, 2004--2006.
• 17: 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]
• 18: Jamaica virtual machine. www.aicas.com/jamaica, 1999--2006.
• 19: J. Kwon, A. Wellings, and S. King. Assessment of the java programming language for use in high integrity systems. Technical Report YCS 341 (2002), University of York, 2002.
• 20: 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
• 21: A Profile for High-Integrity Real-Time Java Programs, Proceedings of the Fourth International Symposium on Object-Oriented Real-Time Distributed Computing, p.15, May 02-04, 2001
• 22: B. K. Rosen , M. N. Wegman , F. K. Zadeck, Global value numbers and redundant computations, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.12-27, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73562]
• 23: Atanas Rountev , Ana Milanova , Barbara G. Ryder, Points-to analysis for Java using annotated constraints, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.43-55, October 14-18, 2001, Tampa Bay, FL, USA
• 24: M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis., chapter 7, pages 189--234. Prentice-Hall, 1981.
• 25: Bjarne Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.32-41, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237727]
• 26: Mads Tofte, A brief introduction to regions, Proceedings of the 1st international symposium on Memory management, p.186-195, October 17-19, 1998, Vancouver, British Columbia, Canada
• 27: 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]
• 28: John Whaley , Monica S. Lam, Cloning-based context-sensitive pointer alias analysis using binary decision diagrams, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 29: Jianwen Zhu , Silvian Calman, Symbolic pointer analysis revisited, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors

General Terms:
Algorithms, Languages, Reliability, Verification

Keywords:
context sensitive, data-flow analysis, java, pointer analysis, program analysis, real-time specification for java, runtime errors