Abstract
We present a tool for verifying temporal properties on Java/ JML classes by generating automatically JML annotations that ensure the verification of the temporal properties.
Research partially funded by the french ACI GECCOO.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bellegarde, F., Groslambert, J., Huisman, M., Julliand, J., Kouchnarenko, O.: Verification of liveness properties with JML. Technical Report RR-5331, INRIA (2004)
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)
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)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: International Conf. on Software Engineering, pp. 411–420. IEEE Computer Society Press/ACM Press (1999)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. Technical report, Iowa State University, Dept. of Computer Science (1998)
Nelson, G.: Techniques for Program Verification. PhD thesis, Stanford University (1980)
Trentelman, K., Huisman, M.: Extending JML Specifications with Temporal Logic. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 334–348. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giorgetti, A., Groslambert, J. (2006). JAG: JML Annotation Generation for Verifying Temporal Properties. In: Baresi, L., Heckel, R. (eds) Fundamental Approaches to Software Engineering. FASE 2006. Lecture Notes in Computer Science, vol 3922. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11693017_27
Download citation
DOI: https://doi.org/10.1007/11693017_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33093-6
Online ISBN: 978-3-540-33094-3
eBook Packages: Computer ScienceComputer Science (R0)