Using the Bandera Tool Set to Model-Check Properties of Concurrent Java Software
Using the Bandera Tool Set to Model-Check Properties of Concurrent Java Software
复制标题
DOI：
10.1007/3-540-44685-0_5
复制
发表时间：
2001-08
期刊：
影响因子：
--
通讯作者：
J. Hatcliff;Matthew B. Dwyer
中科院分区：
文献类型：
--
作者：
J. Hatcliff;Matthew B. Dwyer
Bandera工具集是程序分析、转换和可视化组件的集成集合，旨在促进对Java源代码进行模型检查的实验。Bandera将Java源代码和用Bandera的临时规范语言形成的软件需求作为输入，并以几种现有模型检查工具（包括Spin[16]、dSpin[6]、SMV[3]和JPF[2]）中的一种的输入语言生成程序模型和规范。应用程序切片和用户可扩展的抽象解释组件来根据被检查的属性定制程序模型。当模型检查器生成错误跟踪时，Bandera在源代码级别呈现错误跟踪，并允许用户沿着跟踪的路径逐级执行代码，同时显示变量值和Java锁对象的内部状态。
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.