对Java并发程序进行模型检测  

Model checking Java concurrent programs

作　　者：周志远[1] 张大方[1] 缪力[1] 

机构地区：[1]湖南大学软件学院,湖南长沙410082

出　　处：《计算机工程与设计》2009年第2期370-373,共4页Computer Engineering and Design

基　　金：国家自然科学基金项目(60673155;90718008)

摘　　要：随着多核处理器的发展,多线程并发程序成为现代程序设计的趋势。但并发线程的执行存在不确定性,传统的测试方法很难发现这类错误。针对这个问题,提出了一种直接分析Java源代码,从中提取并发程序模型的方法;并以此方法为基础开发了工具JTS(Java to SPIN),实现了对Java并发程序的自动化分析和模型检测。实验表明JTS能够成功地检测出Java并发程序中存在的错误并给出相应的错误路径。这项工作给Java并发程序的测试与验证提供了新的途径。With the development ofmulti-core processors, multi-threaded concurrent programs become the trend ofprogramming, But the executions of concurrent programs have nondeterministic, which cause bugs are difficult to find by traditional testing. By analyzing the source code directly, a approach for extracting concurrent models from Java programs is proposed. Based on this approach, a tool called JTS （Java to SPIN） is developed, which implements the automatic analysis and model checking for Java programs. The experiment shows JTS can successfully detect the bugs of concurrent Java programs and present the corresponding traces. A new way is provided to test and verify Java concurrent programs.

关 键 词：模型检测 程序分析 并发程序 程序验证 软件测试 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]