摘要：构建组合服务的形式化模型是对其进行验证的前提与基础,然而缺乏统一的构建框架使得建模过程变得难以把握且无法实现自动化。通过对确定型有限自动机的扩展,建立了用于描述OWL-S过程模型的有限迁移系统——服务过程自动机,为组合服务的形式化建模提供了统一框架和自动化基础。同时,通过分析服务过程自动机的可接受位置及其在组合过程中可能产生的约束,将相容性划分为三个等级,从而能够在不同强度的可靠性要求下进行组合服务的验证工作。

关键词：服务组合验证 形式化模型 服务过程自动机 相容性分析 

单位：福建工程学院信息科学与工程学院 福建福州350118 贵州师范大学数学与计算机科学学院 贵州贵阳550001 贵州大计算机科学与技术学院 贵州贵阳550025