Treffer: Using the Bandera Tool Set to model-check properties of concurrent Java software

Title:
Using the Bandera Tool Set to model-check properties of concurrent Java software
Authors:
HATCLIFF, John, DWYER, Matthew
Source:
CONCUR 2001 - concurrency theory (Aalborg, 20-25 August 2001)Lecture notes in computer science. :39-58
Publisher Information:
Berlin: Springer, 2001.
Publication Year:
2001
Physical Description:
print, 22 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Logiciel, Software, Systèmes informatiques et systèmes répartis. Interface utilisateur, Computer systems and distributed systems. User interface, Analyse programme, Program analysis, Análisis programa, Codage, Coding, Codificación, Interface utilisateur, User interface, Interfase usuario, Langage JAVA, JAVA language, Lenguaje JAVA, Langage spécification, Specification language, Lenguaje especificación, Machine abstraite, Abstract machine, Máquina abstracta, Simultanéité informatique, Concurrency, Simultaneidad informatica, Spécification modèle, Model specification, Especificación modelo, Spécification programme, Program specification, Especificación programa, Système réparti, Distributed system, Sistema repartido, Transformation programme, Program transformation, Transformación programa, Visualisation, Visualization, Visualización, Bandera tool set
Document Type:
Konferenz Conference Paper
File Description:
text
Language:
English
Author Affiliations:
SAnToS Laboratory, Department of Computing and Information Sciences, Kansas State University, 234 Nichols Hall, Manhattan KS, 66506, United States
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=14047040
Rights:
Copyright 2002 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.14047040
Database:
PASCAL Archive

Weitere Informationen

The Bandera Tool Set is an integrated collection of program analysis, transformation, and visualization components designed to facilitate experimentation with model-checking Java source code. Bandera takes as input Java source code and a software requirement formalized in Bandera's temporal specification language, and it generates a program model and specification in the input language of one of several existing model-checking tools (including Spin [16], dSpin [6], SMV [3], and JPF [2]). Both program slicing and user extensible abstract interpretation components are applied to customize the program model to the property being checked. When a model-checker produces an error trail, Bandera renders the error trail at the source code level and allows the user to step through the code along the path of the trail while displaying values of variables and internal states of Java lock objects. In this tutorial paper, we use a simple concurrent Java program to illustrate the functionality of the main components of Bandera and how to interact the tool set using its graphical user interface.