面向服务体系构架SOA作为整合已有不同系统的一种构架被提出来,主要是解决企业中信息孤岛问题。BPEL是业务流程执行语言用来描述SOA的服务协作模型,实现对各个系统业务流程的编排。但其随着整合遗产系统的增多和业务流程复杂性的增加,BPEL建模也变得异常复杂,同时,因其缺乏形式化的语义描述,极易潜藏一些逻辑错误。简化BPEL建模并自动验证其逻辑正确性将有利于SOA的普及应用。MDA作为一种模型驱动开发构架,它的核心思想是抽象出与具体实现技术无关的PIM层模型,通过转换工具将PIM层模型自动的转换到PSM平台相关层模型。本文给出了一种基于MDA的SOA服务协作模型的构建方法,首先使用UML活动图描述服务协作模型的交互过程,以构建SOA服务协作的PIM模型;然后,通过建立活动图元模型元素与BPEL元模型元素之间的映射规则,以XMI作为标准交换文件,利用EMF及MTF模型框架作为模型转换引擎,将SOA服务协作模型自动转换为BPEL模型即PSM模型。本文还对BPEL的逻辑正确性的验证方法进行了研究,通过将BPEL转换为有色Petri网,利用Petri网工具实现BPEL模型逻辑正确性的自动化验证。由于采用了Petri网工具内置的函数实现分支的跳过处理,简化了BPEL模型到Petri网的转换的复杂性,使其更有利于BPEL的验证。本文利用网上购书的原型系统进行实例验证,利用活动图对网上购物车、银行收费和物流等服务进行了SOA服务协作模型建模,并成功地转换成了BPEL,利用有色Petri网工具进行了结果BPEL的逻辑正确性验证,通过与XSLT的转换方法对比,表明本文给出的方法的可行性和高效性。