Titre du document / Document title

Extending JML for modular specification and verification of multi-threaded programs

Auteur(s) / Author(s)

RODRIGUEZ Edwin ⁽¹⁾ ; DWYER Matthew ⁽²⁾ ; FLANAGAN Cormac ⁽³⁾ ; HATCLIFF John ⁽¹⁾ ; LEAVENS Gary T. ⁽⁴⁾ ; ROBBY ⁽¹⁾ ;

Affiliation(s) du ou des auteurs / Author(s) Affiliation(s)

⁽¹⁾ Department of Computing and Information Sciences, Kansas State University, ETATS-UNIS
⁽²⁾ Department of Computer Science and Engineering, University of Nebraska-Lincoln, ETATS-UNIS
⁽³⁾ Computer Science Department, University of California at Santa Cruz, ETATS-UNIS
⁽⁴⁾ Department of Computer Science, Iowa State University, ETATS-UNIS

Résumé / Abstract

The Java Modeling Language (JML) is a formal specification language for Java that allows developers to specify rich software contracts for interfaces and classes, using pre- and postconditions and invariants. Although JML has been widely studied and has robust tool support based on a variety of automated verification technologies, it shares a problem with many similar object-oriented specification languages-it currently only deals with sequential programs. In this paper, we extend JML to allow for effective specification of multi-threaded Java programs. The new constructs rely on the non-interference notion of method atomicity, and allow developers to specify locking and other non-interference properties of methods. Atomicity enables effective specification of method pre- and postconditions and supports Hoare-style modular reasoning about methods. Thus the new constructs mesh well with JML's existing features. We validate the specification language design by specifying the behavior of a number of complex Java classes designed for use in multi-threaded programs. We also demonstrate that it is amenable to automated verification using model checking technology.

Revue / Journal Title

Lecture notes in computer science   ISSN 0302-9743 

Source / Source

Congrès
ECOOP 2005 : object-oriented programming :   ( Glasgow, 25-29 July 2005 )
European conference on object-oriented programming N^o19, Glasgow , ROYAUME-UNI (25/07/2005)
2005  , vol. 3586, pp. 551-576[Note(s) : XVII, 629 p., ] [Document : 26 p.] (39 ref.) ISBN 3-540-27992-X ;  Illustration : Illustration ;

Langue / Language

Anglais

Editeur / Publisher

Springer, Berlin, ALLEMAGNE  (1973) (Revue)
Springer, Berlin, ALLEMAGNE  (2005) (Monographie)

Mots-clés anglais / English Keywords

Atomicity ; Complex number ; Locking ; Invariant ; Modeling ; Confidentiality ; Contract ; Multithread ; Modular programming ; Modelling language ; Model checking ; Computer security ; Object oriented ; Automatic proving ; Specification language ; Formal specification ; Formal language ; JAVA language ; Program verification ; Software development ;

Mots-clés français / French Keywords

Atomicité ; . ; Nombre complexe ; Verrouillage ; Invariant ; Modélisation ; Confidentialité ; Contrat ; Multitâche ; Programmation modulaire ; Langage modélisation ; Vérification modèle ; Sécurité informatique ; Orienté objet ; Démonstration automatique ; Langage spécification ; Spécification formelle ; Langage formel ; Langage JAVA ; Vérification programme ; Développement logiciel ;

Mots-clés espagnols / Spanish Keywords

Atomicidad ; Número complejo ; Fijación ; Invariante ; Modelización ; Confidencialidad ; Contrato ; Multitarea ; Programación modular ; Lenguaje modelización ; Verificación modelo ; Seguridad informatica ; Orientado objeto ; Demostración automática ; Lenguaje especificación ; Especificación formal ; Lenguaje formal ; Lenguaje JAVA ; Verificación programa ; Desarrollo logicial ;

Localisation / Location

INIST-CNRS, Cote INIST : 16343, 35400012441136.0240