Symbolic Animation of JML Specifications

1. Abrial, J.-R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)

   Book  MATH  Google Scholar 

2. Ambert, F., Bouquet, F., Chemin, S., Guenaud, S., Legeard, B., Peureux, F., Vacelet, N., Utting, M.: BZ-TT: A Tool-Set for Test Generation from Z and B using Contraint Logic Programming. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 105–120. Springer, Heidelberg (2002)

   Google Scholar 

3. Bouquet, F., Dadeau, F., Groslambert, J.: Checking JML Specifications with B Machines. In: Treharne, H., King, S., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 435–454. Springer, Heidelberg (2005)

   Google Scholar 

4. Bouquet, F., Dadeau, F., Legeard, B., Utting, M.: JML-Testing-Tools: a Symbolic Animator for JML Specifications using CLP. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 551–556. Springer, Heidelberg (2005)

   Chapter  Google Scholar 

5. Cheon, Y., Leavens, G.T.: A Runtime Assertion Checker for the Java Modeling Language (JML). In: Arabnia, H.R., Mun, Y. (eds.) Proceedings of the International Conference on Software Engineering Research and Practice (SERP 2002), Las Vegas, Nevada, USA, June 24-27, pp. 322–328. CSREA Press (2002)

   Google Scholar 

6. Gogolla, M., Richters, M.: Development of UML Descriptions with USE. In: Shafazand, H., Tjoa, A.M. (eds.) EurAsia-ICT 2002. LNCS, vol. 2510, pp. 228–238. Springer, Heidelberg (2002)

   Chapter  Google Scholar 

7. Gray, J., Schach, S.: Constraint Animation Using an Object-Oriented Declarative Language. In: Proceedings of the 38th Annual ACM SE Conference, Clemson (April 2000)

   Google Scholar 

8. Hazel, D., Strooper, P., Traynor, O.: Possum: An Animator for the SUM Specification Language. In: Proceedings of the Fourth Asia-Pacific Software Engineering and International Computer Science Conference, pp. 42–51 (1997)

   Google Scholar 

9. Leavens, G.T., Baker, A.L., Ruby, C.: JML: a Java Modeling Language. In: Formal Underpinnings of Java Workshop (at OOPSLA 1998) (October 1998)

   Google Scholar 

10. Legeard, B., Peureux, F., Utting, M.: Controlling Test Case Explosion in Test Generation from B Formal Models. The Journal of Software Testing, Verification and Reliability 14(2) (2004) (To appear)

    Google Scholar 

11. McComb, T., Smith, G.: Animation of Object-Z Specifications Using a Z Animator. In: International conference on Software Engineering and Formal Methods (SEFM 2003). IEEE Computer Society, Los Alamitos (2003)

    Google Scholar 

12. Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, Englewood Cliffs (1997)

    MATH  Google Scholar 

13. Robby, Rodríguez, E., Dwyer, M.B., Hatcliff, J.: Checking Strong Specifications Using an Extensible Software Model Checking Framework. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 404–420. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

14. Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Addison-wesley, Reading (1999)

    Google Scholar 

15. Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall, Englewood Cliffs (1992)

    Google Scholar 

16. Wahls, T., Leavens, G.T., Baker, A.L.: Executing Formal Specifications with Concurrent Constraint Programming. Automated Software Engineering 7(4), 315–343 (2000)

    Article  MATH  Google Scholar 

17. Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modeling with UML. Addison-Wesley, Reading (1988)

    Google Scholar 

Download references