作者：雷丽晖; 段振华组合web服务投影时序逻辑形式化验证
摘要：针对编制方式生成的组合Web服务需要用一个工作流引擎执行这个特征，对投影时序逻辑进行了扩展，并用扩展投影时序逻辑描述和验证组合Web服务．将组合Web服务视为一个基于过程的工作流，将工作流引擎与组合web服务组成部分的一次不可分割的消息交互抽象为一个原子过程．用扩展投影时序逻辑公式描述原子过程，用扩展投影时序逻辑操作符定义过程组合规则、连接过程描述公式，得到组合Web服务描述公式．通过模拟组合Web执行，可验证组合Web服务满足系统的需求和性质，为提高组合Web服务设计的可靠性提供了依据．
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
