Extending JML Specifications with Temporal Logic

Kerry Trentelman, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

31 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationAlgebraic Methodology and Software Technology, 9th International Conference, AMAST 2002, Saint-Gilles-les-Bains, Reunion Island, France, September 9-13, 2002, Proceedings
EditorsHélène Kirchner, Christophe Ringeissen
PublisherSpringer Singapore
Pages334-348
Number of pages15
ISBN (Electronic)978-3-540-45719-0
ISBN (Print)978-3-540-44144-1
DOIs
Publication statusPublished - 2002
Externally publishedYes
Event9th International Conference on Algebraic Methodology and Software Technology, AMAST 2002 - Saint-Gilles-les-Bains, France
Duration: 9 Sep 200213 Sep 2002
Conference number: 9

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume2422

Conference

Conference9th International Conference on Algebraic Methodology and Software Technology, AMAST 2002
Abbreviated titleAMAST 2002
CountryFrance
CitySaint-Gilles-les-Bains
Period9/09/0213/09/02

Fingerprint

Dive into the research topics of 'Extending JML Specifications with Temporal Logic'. Together they form a unique fingerprint.

Cite this