Skip to main content
SpringerLink
Log in

Extending JML Specifications with Temporal Logic

  • Conference paper
  • First Online:
Algebraic Methodology and Software Technology (AMAST 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2422))

Abstract

This paper proposes an extension of the Java Modeling Language (JML) with temporal specifications. The extension is inspired by the patterns and specification language used within the Bandera project, and is especially tailored to specify properties of Java(Card) programs; for example, it allows the exceptional behaviour of methods to be specified. In the tradition of JML, the extension has been designed to be simple, easy and intuitive to use for software engineers. As an example, we show how the JML extension can be used to specify temporal aspects of the JavaCard API. Later, a semantics for the extension is discussed. We show how to translate a subset of the extension back into standard JML, thus allowing the re-use of existing verification techniques for JML. For the ‘new’ part of the language, a trace-based semantics is given.

Supported by the Australian Research Council and Gemplus France via an APA(I) scholarship, and a visiting fellowship from INRIA Sophia-Antipolis.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. D. Bartetzko, C. Fischer, M. Möller, and H. Wehrheim. Jass—Java with Assertions. In K. Havelund and G. Roşu, editors, Runtime Verification, number 55(2) in ENTCS. Elsevier, 2001.

    Google Scholar 

  2. J. Corbett, M. Dwyer, J. Hatcliff, S. Laubach, C. Păsăreanu, Robby, and H. Zheng. Bandera: Extracting finite-states models from Java source code. In M. Jazayeri and A. Wolf, editors, 22nd International Conference on Software Engineering, pages 439–448. ACM Press, June 2000.

    Google Scholar 

  3. J. Corbett, M. Dwyer, J. Hatcliff, and Robby. Expressing Checkable Properties of Dynamic Systems: the Bandera Specification Language. Technical Report 2001-04, Kansas State University, Dept. of Comp. and Info. Sc., 2001.

    Google Scholar 

  4. M. Dwyer, G. Avrunin, and J. Corbett. Property Specification Patterns for Finitestate Verification. In M. Ardis, editor, 2nd Workshop on Formal Methods in Software Practice, pages 7–15, March 1998.

    Google Scholar 

  5. K. Havelund and G. Roşu. Java PathExplorer—A Runtime Verification Tool. In 6th Intnl. Symp. on AI, Robotics and Automation in Space, June 2001.

    Google Scholar 

  6. C. A. R. Hoare. Proofofcorrect ness of data representations. Acta Informatica, 1:271–281, 1972.

    Article  MATH  Google Scholar 

  7. M. Huisman. Reasoning about Java Programs in Higher Order Logic with PVS and Isabelle. PhD thesis, University of N0ijmegen, 2001.

    Google Scholar 

  8. M. Huisman and B. Jacobs. Java Program Verification via a Hoare Logic with Abrupt Termination. In Fundamental Approaches to Software Engineering, number 1783 in LNCS, pages 284–303. Springer, 2000.

    Chapter  Google Scholar 

  9. M. Huisman, B. Jacobs, and J. van den Berg. A Case Study in Class Library Verification: Java’s Vector Class. Software Tools for Technology Transfer, 3/3:332–352, 2001.

    MATH  Google Scholar 

  10. B. Jacobs and E. Poll. A logic for the Java Modeling Language JML. In H. Hussmann, editor, Fundamental Approaches to Software Engineering, number 2029 in LNCS, pages 284–299. Springer, 2001.

    Chapter  Google Scholar 

  11. G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary Design of JML: a Behavioral Interface Specification Language for Java. Technical Report 98-06, Iowa State University, Dept. of Comp. Sc., 1998. Latest revision: August 2001.

    Google Scholar 

  12. G. T. Leavens, K. R. M. Leino, E. Poll, C. Ruby, and B. Jacobs. JML: Notations and Tools Supporting Detailed Design in Java. In ACM Press, editor, OOPSLA 2000 Companion, pages 105–106, October 2000.

    Google Scholar 

  13. J. van Leeuwen, editor. Handbook of Theoretical Computer Science, volume B, chapter 16. Elsevier, 1990.

    Google Scholar 

  14. H. Meijer and E. Poll. Towards a Full Formal Specification of the Java Card API. In I. Attali and T. Jensen, editors, Smart Card Programming and Security (E-smart 2001), number 2140 in LNCS, pages 165–178. Springer, 2001.

    Chapter  Google Scholar 

  15. B. Meyer. Object-Oriented Software Construction. Prentice Hall, 1997.

    Google Scholar 

  16. Robby. Bandera Specification Language: a Specification Language for Software Model Checking. Master’s thesis, Kansas State University, 2000.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Automated Reasoning Group, RSISE, Australian National University, Australia

    Kerry Trentelman

  2. INRIA, Sophia-Antipolis, France

    Marieke Huisman

Authors
  1. Kerry Trentelman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marieke Huisman
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LORIA - CNRS & INRIA, Campus Scientifique, Bâtiment LORIA, BP 239, 54506, Vandoeuvre-lès-Nancy, France

    Hélène Kirchner

  2. LORIA - INRIA, 615, rue du Jardin Botanique, 54602, Villers-lès-Nancy, France

    Christophe Ringeissen

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Trentelman, K., Huisman, M. (2002). Extending JML Specifications with Temporal Logic. In: Kirchner, H., Ringeissen, C. (eds) Algebraic Methodology and Software Technology. AMAST 2002. Lecture Notes in Computer Science, vol 2422. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45719-4_23

Download citation

  • DOI: https://doi.org/10.1007/3-540-45719-4_23

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44144-1

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation