基于TLA的正确性验证方法

• 作者: 庞士焕 张琦 朱相冰 汤萍萍
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: Web服务 TLA BPEL Conversation模型 正确性验证
• 年，卷（期）: 2009,（3）
• 页码范围: 55-58
• 页数: 4页
• 分类号: TP393
• 字数: 4100字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2009.03.013

摘要

随着面向服务的体系结构的发展,有效地组合单个分布的web服务以提供更有价值的服务成为新的热点问题.然而,在这一研究领域还存在诸多问题,比如web服务用哪种方式组合,能否实现自动组合,对组合服务进行正确性验证等等.文中主要是针对组合服务的正确性验证问题,引入时序逻辑TLA.通过把组合服务的BPEL描述转换为TLA可以理解的自动机的形式,这种方法可以很好地验证组合逻辑的正确性以及快速发现死锁等问题.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张琦	西北大学软件学院	19	71	5.0	8.0
2	庞士焕	安徽师范大学教育科学学院	5	3	1.0	1.0
3	朱相冰	安徽师范大学物理与电子信息工程学院	2	2	1.0	1.0
4	汤萍萍	东南大学计算机学院	4	5	2.0	2.0