JMLAutoTest: A Novel Automated Testing Framework Based on JML and JUnit

  • Guoqing Xu
  • Zongyuang Yang
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2931)


Writing specifications using Java Modeling Language has been accepted for a long time as a practical approach to increasing the correctness and quality of Java programs. However, the current JML testing system (the JML and JUnit framework) can only generate skeletons of test fixture and test case class. Writing codes for generating test cases, especially those with a complicated data structure is still a labor-intensive job in the test for programs annotated with JML specifications.

This paper presents JMLAutoTest, a novel framework for automated testing of Java programs annotated with JML specifications. Firstly, given a method, three test classes (a skeleton of test client class, a JUnit test class and a test case class) can be generated. Secondly, JMLAutoTest can generate all nonisomorphic test cases that satisfy the requirements defined in the test client class. Thirdly, JMLAutoTest can avoid most meaningless cases by running the test in a double-phase way which saves much time of exploring meaningless cases in the test. This method can be adopted in the testing not only for Java programs, but also for programs written with other languages. Finally, JMLAutoTest executes the method and uses JML runtime assertion checker to decide whether its post-condition is violated. That is whether the method works correctly.


Hash Table Java Program Operational Profile Pointer Field Generate Test Case 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Cheon, Y.: A Runtime Assertion Checker for the Java Modeling Language. Technical Report 03-09, Department of Computer Science, Iowa State University (April 2003)Google Scholar
  2. 2.
    Cheon, Y., Leavens, G.T.: A simple and practical approach to unit testing: The JML and JUnit way. Technical Report 01-12, Department of Computer Science, Iowa State University (November 2001)Google Scholar
  3. 3.
    Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report TR 98-06i, Department of Computer Science, Iowa State University (June 1998) (last revision: August 2001)Google Scholar
  4. 4.
    Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated Testing Based on Java Predicates. In: Proc. ACM International Symposium on Software Testing and Analysis (ISSTA 2002), July 2002, pp. 123–133 (2002)Google Scholar
  5. 5.
    Deck, M., Whittaker, J.A.: Lessons learned from fifteen years of Cleanroom Testing. Software Testing, Analysis, and Review (STAR) 1997, May 5-9 (1997)Google Scholar
  6. 6.
    Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems,  ch. 12, pp. 175–188. Kluwer, Dordrecht (1999)Google Scholar
  7. 7.
    Bech, K., Gamma, E.: Tested infected: Programmers love writing tests. Java Report 3(7) (July 1998)Google Scholar
  8. 8.
    Goodenough, J., Gerhart, S.: Toward a theory of test data selection. IEEE Transactions on Software Engineering (June 1975)Google Scholar
  9. 9.
    Offutt, J., Abdurazik, A.: Generating tests from UML specifications. In: Proc. Second International Conference on the Unified Modeling Language (October 1999)Google Scholar
  10. 10.
    Horcker, H.M.: Improving software tests using Z specifications. In: Proc. 9th International Conference of Z users, The Z Formal Specification Notation (1995)Google Scholar
  11. 11.
    Marinov, D., Khurshid, S.: TestEra: A novel framework for automated testing of Java programs. In: Proc. 16th IEEE Engineering (ASE), San Diego, CA (November 2001)Google Scholar
  12. 12.
    Peters, D., Parnas, D.L.: Generating a test oracle from program documentation. In: Proc. ISSTA 1994, Seattle, Washington (August 1994)Google Scholar
  13. 13.
    Richardson, D.J.: TAOS: Testing with analysis and oracle support. In: Proc. ISSTA 1994, Seattle, Washington (August 1994)Google Scholar
  14. 14.
    Stocks, P., Carrington, D.: Test template framework: A specification-based test case study. In: Proc. the 1993 International Symposium on Software Testing and Analysis (ISSTA), June 1993, pp. 11–18 (1993)Google Scholar
  15. 15.
    Musa, J.D.: Operational Profiles in Software-Reliability Engineering. IEEE Software, 14–32 (March 1993)Google Scholar
  16. 16.
    NIST/SEMATECH E-Handbook of Statistical Methods (May 2003),
  17. 17.
  18. 18.
    Chillarege, R.: Software testing best practice. Technical Report RC 21457, Center for Software Engineering, IBM Research (April 1999)Google Scholar
  19. 19.
    Banks, D., Dashiell, W., Gallagher, L., Hagwood, C., Kacker, R., Rosenthal, L.: Software testing based on statistical methods. National Institute of Standards and Technology Information Technology Laboratory, Gaithersburg, MD (March 1998)Google Scholar
  20. 20.
    Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice Hall, Englewood Cliffs (1992)Google Scholar
  21. 21.
    Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Addison-Wesley Object Technology Series (1998)Google Scholar
  22. 22.
    Jackson, D., Shlyakhter, I., Shlyakhter, I.: ALCOA: The Alloy constraint analyzer. In: Proc. 22nd International Conference on Software Engineering (ICSE), Limerick, Ireland (June 2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Guoqing Xu
    • 1
  • Zongyuang Yang
    • 1
  1. 1.Software Engineering Lab, The Department of Computer ScienceEast China Normal UniversityShanghaiP.R.China

Personalised recommendations