UML state machine diagram driven runtime verification of Java programs for message interaction consistency

ABSTRACT

In object-oriented programs, we often need to set some restrictions on the temporal orders of the message receiving for objects, which forms a class of safety requirements. In this paper, we use UML state machine diagrams as design specifications, and present an approach to runtime verification of Java programs, which is focused on the temporal order of message receiving based consistency verification between the behavior of state machine diagrams and the program execution traces. In the approach, we first instrument the program under verification so as to gather the program execution traces related to a given state machine diagram. Then we drive the instrumented program by random test cases so as to generate the program execution traces. Finally we check if the collected program execution traces are consistent with the behavior of the state machine diagram, which means that the temporal orders of the message receiving occurring in the program traces are consistent with the ones occurring in the state machine diagram. Our approach can be used to detect not only the program bugs resulting from the wrong temporal orders of message receiving, but also the imperfect state machine models constructed in reverse engineering for legacy systems, and leads to a testing tool which may proceed in a fully automatic fashion.

REFERENCES

• 1: James Rumbaugh , Ivar Jacobson , Grady Booch, The Unified Modeling Language reference manual, Addison-Wesley Longman Ltd., Essex, UK, 1998
• 2: OMG. UML2.0 Superstructure Specification, 2004. www.uml.org.
• 3: Havelund, K. and G. Rosu, editors, Proceedings of First Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, Vol.65, Issue 7, Elsevier, 2001.
• 4: Bernd Finkbeiner, Sriram Sankaranarayanan, Henny Sipma. Collecting Statistics over Runtime Executions. In Electronic Notes in Theoretical Computer Science, Vol.55, Issue 2, Elsevier, 2001.
• 5: Russell C. Bjork. The Simulation of an Automated Teller Machine. http://www.math-cs.gordon.edu/local/courses/cs211/ATMExample/Links.html.
• 6: Detlef Bartetzko, Clemens Fischer, Michael Moller, and Heike Wehrheim. Jass - Java with Assertions. In Electronic Notes in Theoretical Computer Science, Vol.55, Issue 2, Elsevier, 2001.
• 7: Klaus Havelund and Grigore Rou. Monitoring Java Programs with Java PathExplorer. In Electronic Notes in Theoretical Computer Science, Vol.55, Issue 2, Elsevier, 2001.
• 8: M. Kim, S. Kannan, I. Lee, O. Sokolsky and M. Viswanathan. Java-MaC: A Run-time Assurance Tool for Java Programs. In Electronic Notes in Theoretical Computer Science, Vol.55, Issue 2, Elsevier, 2001.
• 9: Marcelo d'Amorim , Klaus Havelund, Event-based runtime verification of java programs, Proceedings of the third international workshop on Dynamic analysis, p.1-7, May 17-17, 2005, St. Louis, Missouri
• 10: David Y. W. Park, Ulrich Stern, Jens U. Skakebak, and David L. Dill. Java Model Checking. In Proceedings of the First International Workshop on Automated Program Analysis, Testing, and Verification, 2000.
• 11: Klaus Havelund and Thomas Pressburger. Model checking JAVA programs using JAVA PathFinder. In International Journal on Software Tools for Technology Transfer, (2000) 2: 366--381.
• 12: Rajeev Alur. Trends and Challenges in Algorithmic Software Verification. In Proceedings of IFIP Working Conference on Verified Software: Theories, Tools, Experiments, 2005, http://vstte.ethz.ch/speakers.html.
• 13: Rajeev Alur , Pavol Černý , P. Madhusudan , Wonhong Nam, Synthesis of interface specifications for Java classes, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.98-109, January 12-14, 2005, Long Beach, California, USA
• 14: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Permissive interfaces, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 15: Stefania Gnesi , Diego Latella , Mieke Massink, Formal Test-Case Generation for UML Statecharts, Proceedings of the Ninth IEEE International Conference on Engineering Complex Computer Systems Navigating Complexity in the e-Engineering Age (ICECCS'04), p.75-84, April 14-16, 2004
• 16: Diego Latella , Mieke Massink, On testing and conformance relations for UML statechart diagrams behaviours, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 17: Philippe Chevalley , Pascale Thévenod-Fosse, Automated Generation of Statistical Test Cases from UML State Diagrams, Proceedings of the 25th International Computer Software and Applications Conference on Invigorating Software Development, p.205-214, October 08-12, 2001
• 18: Y. G. Kim, H. S. Hong, S. M. Cho, D. H. Bae, and S. D. Cha. Test Case Generation from UML State Diagrams. In IEEE Proceedings - Software, 146(4), 1999, pp.187--192.
• 19: Li Xuandong, Wang Linzhang, Qiu Xiaokang, Lei Bin, Yuan Jiesong, Zhao Jianhua, Zheng Guoliang. Runtime Verification of Java Programs for Scenario-Based Specifications. In Proceedings of the 11th International Conference on Reliable Software Technologies (AE2006), LNCS 4006, Springer, 2006, pp.94--106.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: UML

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Object-oriented design methods; State diagrams
      D.2.4 Software/Program Verification
      D.2.5 Testing and Debugging
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Run-time environments

General Terms:
Design, Languages, Management, Verification

Keywords:
UML state machine diagrams, java, runtime verification