高可靠的分布式系统迫切需要模型检查技术来验证程序的时态逻辑性质,以弥补一般软件测试技术之不足。分布式Java程序的模型检查有三个难点:并发过程间程序的可达性分析不可判定,导致分布式程序的控制结构缺乏精确的模型检查算法;Java程序面向对象的特性致使模型提取困难;并发/分布式特性使得谓词抽象算法效率低下。本项目拟采用流分析作为分布式Java程序模型检查的算法基础,研究参数化的并发过程间流分析近似算法以解决并发过程间流分析的不可判定问题。通过类型分析理论研究Java程序多态性问题,提取较精确的并发扩展下推系统模型。针对Java程序的并发结构和实际协议程序特点,提出适用于分布式Java程序的高效谓词抽象算法。开发Java程序模型检查工具,验证分布式系统协议逻辑性质,增强分布式系统可靠性。
{{i.achievement_title}}
数据更新时间:2023-05-31
EBPR工艺运行效果的主要影响因素及研究现状
一种基于多层设计空间缩减策略的近似高维优化方法
复杂系统科学研究进展
基于LS-SVM香梨可溶性糖的近红外光谱快速检测
基于多色集合理论的医院异常工作流处理建模
SPMD程序设计模型——从Fortran到Java
通用Java程序到实时Java程序的对象自动分类和转化方法研究
分布式流处理程序的分析与验证
Java构件的组合模型检验技术研究