Advertisement

Checking JML Specifications with B Machines

  • Fabrice Bouquet
  • Frédéric Dadeau
  • Julien Groslambert
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3455)

Abstract

This paper presents a solution to the lack of tool-support for the JML models verification. We propose an approach for expressing JML specifications within the B abstract machines notation. The B machines generated from the JML can then be checked to ensure their correctness. Thus, we deduce the correctness of the original JML specification, ensured by rewriting rules which give the semantical equivalence of the two models. More generally, this translation can be applied to object-oriented specification languages using before-after predicates.

Keywords

Java Modeling Language JML object-oriented B method specifications abstract machines 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Abr96]
    Abrial, J.-R.: The B-book: assigning programs to meanings. Cambridge University Press, Cambridge (1996)zbMATHCrossRefGoogle Scholar
  2. [B4F03]
    The B4free web site (2003), http://www.b4free.com
  3. [BCC+03]
    Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. In: Arts, T., Fokkink, W. (eds.) Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003). ENTCS, vol. 80, pp. 73–89. Elsevier, Amsterdam (2003)Google Scholar
  4. [BDLU05]
    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) (to appear)CrossRefGoogle Scholar
  5. [BGH+04]
    Bellegarde, F., Groslambert, J., Huisman, M., Kouchnarenko, O., Julliand, J.: Verification of liveness properties with JML. Technical Report RR-5331, INRIA (2004)Google Scholar
  6. [BMvW00]
    Back, R.-J., Mikhajlova, A., von Wright, J.: Class refinement as semantics of correct object substitutability. Formal Aspects of Computing 12, 18–40 (2000)zbMATHCrossRefGoogle Scholar
  7. [BRL03]
    Burdy, L., Requet, A., Lanet, J.-L.: Java applet correctness: A developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 422–439. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  8. [CDD+03]
    Couchot, J.-F., Dadeau, F., Déharbe, D., Giorgetti, A., Ranise, S.: Proving and debugging set-based specifications. In: proceedings of the Sixth Brazilian Workshop on Formal Methods (WMF 2003), May 2003. Electronic Notes in Theoretical Computer Science, vol. 95, pp. 189–208 (2003)Google Scholar
  9. [Cle01]
    Clearsy, Europarc de Pichaury 13856 Aix-en-Provence Cedex 3 - France. Atelier B Technical Support version 3 (May 2001), http://www.atelierb.societe.com
  10. [GJS00]
    Gosling, J., Joy, B., Steele, G.: The Java Language Specification, 2nd edn. Java Series. Sun Microsystems (2000)Google Scholar
  11. [HJ00]
    Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 284–303. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  12. [LBR99]
    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, pp. 175–188. Kluwer Academic Publishers, Boston (1999)Google Scholar
  13. [LP02]
    Laleau, R., Polack, F.: Coming and going from UML to B: a proposal to support traceability in rigorous IS development. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 517–534. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  14. [Mey97]
    Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, Englewood Cliffs (1997)zbMATHGoogle Scholar
  15. [MPMU04]
    Marché, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming 58(1-2), 89–106 (2004)zbMATHCrossRefGoogle Scholar
  16. [NS99]
    Neilson, D., Sorensen, I.H.: The B-Technologies: a system for computer aided programming. B-Core (UK) Limited, Kings Piece, Harwell, Oxon, OX11 0PA (1999), http://www.b-core.com/btoolkit.html
  17. [RJB99]
    Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. addison-wesley edition, Reading (1999)Google Scholar
  18. [WK98]
    Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modeling with UML. Addison-Wesley, Reading (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Fabrice Bouquet
    • 1
  • Frédéric Dadeau
    • 1
  • Julien Groslambert
    • 1
  1. 1.Laboratoire d’Informatique (LIFC)Université de Franche-Comté, CNRS – INRIABesançon cedexFrance

Personalised recommendations