[发明专利]语义Web服务组合的自动验证方法及其系统

摘要

本发明提供一种语义Web服务组合的自动验证方法及其系统，将OWL‑S描述的Web服务转化为一台原子过程自动机，将原子过程自动机组合为组合过程自动机；消除组合过程自动机的冗余并发和同步迁移，获得优化模型；依据用户限定的相容性要求，确定组合过程自动机的可接受位置集合；依据用户限定的有效性要求，确定逻辑公式CSV；将优化模型转换为UPPAAL的建模语言；将可接受位置集合和逻辑公式CSV表示为CTL公式；将建模语言描述的组合服务模型与CTL公式输入UPPAAL进行验证；对OWL‑S中的原子过程与组合过程的描述更具体完整，可以无差异地参加组合运算，支持逻辑公式和表达式，描述能力更强，提高了验证的效率。

主权项

一种语义Web服务组合的自动验证方法，其特征在于：包括如下步骤：步骤10、将OWL‑S描述的Web服务即原子过程转化为一台原子过程自动机，然后根据不同的控制结构，将原子过程自动机组合为组合过程自动机；步骤20、消除组合过程自动机的冗余并发和同步迁移，获得优化模型；步骤30、依据用户限定的相容性要求，确定组合过程自动机的可接受位置集合；步骤40、依据用户限定的有效性要求，确定有效的逻辑公式CSV，所述有效的逻辑公式CSV＝(INFOS,EFFECTS)，其中：INFOS为一组要求组合服务产生的语义信息集合；EFFECTS为一组逻辑公式，该逻辑公式描述要求组合服务必须达到的限定效果；步骤50、将所述获得优化模型转换为UPPAAL的建模语言；步骤60、将可接受位置集合和逻辑公式CSV表示为CTL公式：相容性变量cptyVari∈{unconcerned,incompatible,weak,ordinary,strong}，表示UTAi当前的相容性：unconcerned表示该UTAi所描述的并行分支还未被激活或已经结束，incompatible表示不相容，weak表示弱相容，ordinary表示普通/自定义相容，strong表示强相容，可以用取值范围为[0,4]的整型变量来表示相容性变量，数值0～4依次代表incompatible、weak、ordinary、strong、unconcerned，三种相容性在UPPAAL中可描述为：满足强相容性；满足普通/自定义相容性；满足弱相容性；当组合服务完成一次完整运行后没有迁移再发生，组合服务进入死锁状态，在UPPAAL中以deadlock关键字表示，故可将完全/部分相容性表示为CTL公式F1，如下：其中cptyVari为相容性变量；对于有效性CSV＝(INFOS,EFFECTS)，完全/部分有效且强/普通/弱相容，表示为CTL公式F2，如下：所述A的语义是“所有运行”，E的语义是“存在至少一个运行”；所述UTAi表示第i台时间自动机；f(c)表示c的映射；步骤70、将建模语言描述的组合服务模型与CTL公式输入UPPAAL进行验证；若验证结果为完全相容且有效，则该组合服务满足用户需求；若验证结果为部分相容且有效，则可根据验证结果生成信息交互引擎，引导组合服务的运行轨迹，达到用户要求；若验证结果是不满足相容且有效，则该组合服务无法满足用户需求。