摘要: 以Web服务技术为代表的面向服务的计算范型是分布式系统和软件集成领域技术进步的一个里程碑。服务作为一种自描述、平台无关的网络化构件可使分布式应用具有更好的复用性和开放性。构造面向服务应用主要通过服务组合语言来完成。主流的服务组合语言包括BPEL和BPML。特别是BPEL，目前已经成为业界事实标准。程序正确性问题一直是软件工程领域研究的重点。在面向服务计算领域，我们同样需要确保构造的BPEL程序满足在需求中定义的系统属性。对该问题典型的解决手段是通过验证（verification）：把程序转换为形式模型后检查其和形式系统属性的一致性。在该领域，我们已经提出了一种简单、直观，基于时态模式的形式化系统属性定义语言PROPOLS （Pattern Based Property Specification and Verification for Services），并把其应用于BPEL的验证。另一种确保程序满足系统属性的技术是综合（synthesis）：把一种形式规范在一定的抽象等级（半）自动转换为另一种，同时在目标规范中保留源规范的显著属性。和验证技术相比较，综合可以给开放人员带来更多的好处：通过综合产生的目标规范不仅保留了源规范的属性，而且可以作为设计或者编程阶段的半成品使用。本文提出一种基于时态业务规则（Temporal Business Rules）的综合产生服务组合过程模型的方法和实现框架。描述时态业务规则的语言是PROPOLS，通过该语言可以定义业务活动的出现或者时序模式。其中每一个时态业务规则的行为语意可以通过一个有限状态自动机来表示；而一组规则的行为模型则可以通过组合各个规则对应的自动机来描述。通过搜索规则行为模型的可接受路径，我们可以得到一组可能的程序执行路径。再通过基于模式的分支识别技术和并行结构识别技术，我们可以得到一个较完整的过程模型。由于时态业务规则是一种松散定义，他们不足以精确完全地定义系统属性，因此产生过程模型的全过程无法达到完全自动，其中依然需要人为参与动作，比如引入新的规则或选择合适的路径。但这些人为参与动作都较简单，完全可以由没有任何形式方法知识的人实现。最后，产生的过程模型可以通过业务活动附带的本体知识搜索可复用的Web服务进一步转换为BPEL程序。本文还讨论了该综合方法和框架在欧盟第6框架研究项目OPUCE（Open Platform for User-centric service Creation and Execution）中的应用及其性能测试。总之，本文的主要贡献是提出了一种从需求模型（也就是时态业务规则）半自动产生设计模型（也就是服务组合过程模型）的方法及其实现框架。该方法具有相当的易用性：不仅有直观的系统属性定义语言，而且可以半自动地产生满足系统属性的过程模型，而需要人为参与的活动仅包括规则定义和结果筛选。