JML2B: Checking JML Specifications with B Machines | SpringerLink
Skip to main content
Springer Nature Link
Log in

JML2B: Checking JML Specifications with B Machines

  • Conference paper
B 2007: Formal Specification and Development in B (B 2007)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4355))

Included in the following conference series:

  • 511 Accesses

Abstract

This paper introduces a tool, named JML2B, destined to check the consistency of JML specifications. JML2B is a solution to the lack of tool-support for the JML models verification. Our tool translates JML specifications into the B abstract machines notation. The generated B machines can then be checked to ensure their correctness. When the proof fails, it is possible to retrieve the mistakes in the original JML specification.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. 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: FMICS 2003. ENTCS, vol. 80, pp. 73–89. Elsevier, Amsterdam (2003)

    Google Scholar 

  2. 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 

  3. Bouquet, F., Dadeau, F., Groslambert, J., Julliand, J.: Safety property driven test generation from JML specifications. In: Havelund, K., Núñez, M., Roşu, G., Wolff, B. (eds.) FATES 2006 and RV 2006. LNCS, vol. 4262, pp. 225–239. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  4. Bouquet, F., Dadeau, F., Legeard, B., Utting, M.: Symbolic animation of JML specifications. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, Springer, Heidelberg (2005)

    Google Scholar 

  5. Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Behavioral Specifications of Businesses and Systems, pp. 175–188. Kluwer, Dordrecht (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire d’Informatique (LIFC), Université de Franche-Comté, CNRS – INRIA Cassis Project, 16, route de Gray, 25030, Besançon cedex, France

    Fabrice Bouquet, Frédéric Dadeau & Julien Groslambert

Authors
  1. Fabrice Bouquet
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frédéric Dadeau
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Julien Groslambert
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LIFC, Université de Franche-Comté, 16, route de Gray, F-25030, Besançon Cedex, France

    Jacques Julliand

  2. LIFC – TFC Team, 16 route de Gray, F-25030, Besançon

    Olga Kouchnarenko

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bouquet, F., Dadeau, F., Groslambert, J. (2006). JML2B: Checking JML Specifications with B Machines. In: Julliand, J., Kouchnarenko, O. (eds) B 2007: Formal Specification and Development in B. B 2007. Lecture Notes in Computer Science, vol 4355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11955757_31

Download citation

  • DOI: https://doi.org/10.1007/11955757_31

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-68760-3

  • Online ISBN: 978-3-540-68761-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics