基于JPF的Java程序验证
肖美华; 尹传文; 舒良春; 胡波; 邹芳红
南昌大学信息工程学院； 先锋软件股份有限公司；
XIAO mei-hua1,2,YIN chuan-wen1,SHU liang-chun1,HU Bo2,ZOU fang-hong2(1.School of Information Engineering,Nanchang University,Nanchang 330031,China;2.Ahead software co.,Ltd.,Nanchang 330041,China)
摘要 形式化方法是提高并发系统的安全性与可靠性的重要手段。JPF(Java Pathfinder)是一种精确的Java字节码状态模型检测工具。在阐述JPF工作原理的基础上,提出了一种适用于JPF的Java程序模型检测方法,包括Java程序模型的建立、状态空间搜索算法的扩展和配置,开发了Java程序反例轨迹
关键词 ：
形式化方法 ,
深度优先搜索 ,
Java路径探测器 ,
启发式搜索 ,
模型检测
Abstract ：Formal methods is one of the most important ways to promote the safety and reliability of concurrent system.JPF(Java Pathfinder) is a kind of explicit state model checker for Java bytecode.Based on the introduction of the working principles of JPF,this pa
Key words ：
model checking
heuristic search；
formal methods
depth first search
Jave pathfinder
出版日期: 2010-03-28
引用本文:
肖美华; 尹传文; 舒良春; 胡波; 邹芳红. 基于JPF的Java程序验证[J]. 南昌大学学报（工科版）, 2010, 32(01): 1-.
链接本文:
http://qks.ncu.edu.cn/Jwk_xbgkb/CN/ 或 http://qks.ncu.edu.cn/Jwk_xbgkb/CN/Y2010/V32/I01/1
2010, Vol. 32 