基于流分析的分布式Java程序模型检查技术研究

高可靠的分布式系统迫切需要模型检查技术来验证程序的时态逻辑性质，以弥补一般软件测试技术之不足。分布式Java程序的模型检查有三个难点：并发过程间程序的可达性分析不可判定，导致分布式程序的控制结构缺乏精确的模型检查算法；Java程序面向对象的特性致使模型提取困难；并发/分布式特性使得谓词抽象算法效率低下。本项目拟采用流分析作为分布式Java程序模型检查的算法基础，研究参数化的并发过程间流分析近似算法以解决并发过程间流分析的不可判定问题。通过类型分析理论研究Java程序多态性问题，提取较精确的并发扩展下推系统模型。针对Java程序的并发结构和实际协议程序特点，提出适用于分布式Java程序的高效谓词抽象算法。开发Java程序模型检查工具，验证分布式系统协议逻辑性质，增强分布式系统可靠性。