Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
JAG: JML Annotation Generation for Verifying Temporal Properties
[go: Go Back, main page]

JAG: JML Annotation Generation for Verifying Temporal Properties *

Alain Giorgetti
Julien Groslambert

January 13, 2007

*Research partially funded by the french ACI GECCOO

JAG is a JML (Java Modeling Language - http://www.jmlspecs.org) annotation generator for verifying temporal properties on Java classes. JAG consists of many translators that transform dynamic properties into standard JML annotations that ensure the satisfaction of these properties.

Historically, the first input language of JAG was JTPL (Java Temporal Pattern Language), an adaptation to Java of a fragment of LTL (Linear Temporal Logic), first introduced in [5]. This temporal logic language, inspired by Dwyers Specification Pattern [2], can deal with exceptional termination of methods and can express both safety and liveness properties The translation is described in details in [5] for safety properties and in [1] for liveness properties.

The current version supports other input formats (see below for details).

1 Download

WARNING: JAG uses embedded third-party Java packages working only with Java VM 1.4.2_**. Make sure you always use such a Java virtual machine, by running the
java -version

command first.

JAG version 0.1

The beta release 0.1 is available here for download (for Java VM 1.4.1 or 1.4.2).

jag-release.jar

It has been successly tested with Sun (Hotspot) JVM version 1.4.1_02.

Launch JAG graphical interface using the following command:
java -jar jag-release.jar

This version includes the following features:

This version has been presented at FASE’06 [3], see  http://dx.doi.org/10.1007/11693017_27 and http://lifc.univ-fcomte.fr/publis/pub/2006/RT2006-02.pdf for the french version.

JAG version 0.2 (NEW)

JAG 0.2 additionally supports Buchi automata input, as presented at JFLA’06.

Download and extract the file

JAG02.zip

as the JAG02 folder.

Then, move to that folder and launch the JAG graphical interface with the following command:
java -jar jag-release.jar

Remember that your Java VM version should be 1.4.2_**.

2 Documentation

Most of the information about this tool can be found in the research papers published about or around it [4, 3].

See also this short tutorial: tutorial/index.html.

3 Examples

3.1 For JAG 0.1 and more

The following zip file contains a Java/JML class and temporal properties that can be verified on this class with the JAG tool, version 0.1 or more.

example/TransactionSystem/transactionSystemBuffer.zip

This archive contains:

3.2 For JAG 0.2 and more

The distribution zip file contains a folder named “example” and containing examples of input and expected output files.

4 Related publications

References

[1]   F. Bellegarde, J. Groslambert, M. Huisman, O. Kouchnarenko, and J. Julliand. Verification of temporal properties with JML. Software and System Modelling, 2005. submited.

[2]   M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property specifications for finite-state verification. In ICSE, pages 411–420, 1999.

[3]   A. Giorgetti and J. Groslambert. JAG: JML Annotation Generation for Verifying Temporal Properties. In FASE, LNCS, pages 373–376. Springer, 2006.

[4]   A. Giorgetti and J.Groslambert. JAG : Génération d’annotations JML pour vérifier des propriétés temporelles. In AFADL’06, 2006. tool session.

[5]   K. Trentelman and M. Huisman. Extending JML Specifications with Temporal Logic. In AMAST’02, number 2422 in LNCS, pages 334–348. Springer, 2002.