基于Pi-演算的THP协议形式化建模与验证
广受关注的Web服务事务处理常因资源死锁而导致资源浪费、利用率低和事务成功率低,Web服务事务处理的资源协调研究越来越活跃。形式化方法对于减少设计错误,提高系统可信度是一种有效的方法。讨论了THP协议与Pi-演算元素的对应关系,说明了利用Pi-演算建立Web服务事务资源协调模型的规则,最后使用Pi-演算对THP协议框架进行形式化建模,并利用形式化工具对建立的模型是否满足无死锁性进行了验证,进一步体现了THP协议在Web服务事务资源协调中的独特优势。
THP协议 Pi-演算 形式化方法 模型检测 Web服务 事务处理
赵健 袁敏 黄志球
南京航空航天大学信息科学与技术学院 南京 210016
国内会议
广州
中文
593-597
2008-11-11（万方平台首次上网日期，不代表论文的发表时间）