在面向服务计算的理念和技术框架下,业务流程(business process)将人、计算机和网络联接以完成特定的业务功能,应用十分广泛。业务流程设计过程包括软件服务选择和复用、流程约束设计与实现、长事务及补偿设计等三个重要方面。本文围绕这三个重要方面、针对如何改善业务流程设计的关键技术问题开展研究工作。首先,在软件服务选择和复用方面,我们针对业务流程中服务的行为调控问题开展研究。面向服务的业务流程的重要特性就是,将软件模块包装为Web服务的方式加以调用和组合,以实现软件之间的松耦合。而在完成业务逻辑的定义之后,需要选择恰当的服务以组合完成特定的业务功能。在组合软件服务时,服务的行为接口可能与流程期望不一致：业务流程仅需要服务的部分行为,而待组合的目标服务却不能保证该行为的发生。我们提出了一个场景驱动的服务行为调控途径,其中用户对服务行为的需求通过UML顺序图场景规约描绘。首先,基于目标服务的BPEL行为规约构造表示服务行为的BPEL-Petri网模型(简称BPN模型)。其次,基于并发变迁分析BPN模型上表示服务行为的路径,并通过遍历BPN模型获取包含UML顺序图描绘场景的服务行为集合。最后,根据行为分析的结果构建调控服务,通过在运行时监听、检查并过滤用户与目标服务的消息交互,从目标服务中抽取或过滤顺序图描绘的场景。在此基础上,我们开发了原型工具BASIS,以支撑场景驱动的服务行为调控途径,并通过实例研究展示了该方法的可行性。其次,在流程约束设计与实现方面,我们研究的问题是如何保持业务流程中数据的一致性。在选定了流程中需要的服务,并保证这些服务能够满足业务逻辑需求之后,业务流程的设计需要实现与业务逻辑对应的工作流和数据约束,同时在业务流程的运行中保持这些约束。数据在业务流程中扮演了关键的角色,数据正确性是业务流程正确性的基础。数据的正确性约束往往通过数据完整性约束,在业务流程设计开发阶段定义。传统的业务流程中,数据完整性约束通过底层数据库支持系统来维护,其不足之处在于：(1)当数据库检测到了数据一致性被违反时,往往不易从业务流程中找出原因：(2)业务流程中的分布式数据上的一致性难以通过现有的分布式数据库管理系统维护；(3)当业务流程中的数据与其它应用共享数据存储时,不应假设共享存储服务能够保证特定业务的数据完整性约束。我们研究了在业务流程的执行中保证数据完整性约束的两种强化机制。首先,对于给定的一组数据完整性约束,针对声明式(基于规则)业务流程语言,我们设计了卫式注入的方法。该方法将一些特定的谓词公式注入到业务流程活动的卫式条件中,以强化数据更新活动的使能条件,从而约束流程执行。其次,如果业务流程以过程式(基于工作流)的语言(如BPEL)设计,则可以扩展卫式注入的方法,将数据一致性检查尽可能的提前。以卫式注入机制为基础,我们提出了业务流程数据一致性调控机制,通过有界的符号执行,检查后续执行中是否会有修改操作违反数据一致性约束。借助这两个方法,强化之后的业务流程对数据库的任何更新都不会违反数据完整性约束。此外,这两个方法是“保守完备”的,即尽可能多地保留了原流程中满足数据完整性约束的运行。最后,在长事务及补偿设计方面,我们研究的问题是长事务的补偿(compensation)设计及正确性保障。事务是业务流程中的关键环节,它将一组活动整合以表现出特有的行为属性(如原子性、一致性等)。业务流程中的事务被称为长事务,是因为这些事务往往运行时间较长,并与外界有交互。由于长事务的开放性、长时间和共享性等特性,在出错时不能将所有系统状态自动回滚,通常需要系统补偿的机制。补偿是一段特殊的流程,在长事务发生错误时调用。已有长事务补偿方面的工作主要存在两方面问题：(1)缺乏长事务应满足的事务特性的恰当定义,即对错误处理和补偿应表现的效果没有恰当的定义,现有工作或是过强地假设整个系统状态都能够撤销,或是过弱地对错误处理和补偿流程的效果不做要求；(2)长事务的补偿设计缺少指导性的原理,现有工作或是要求为所有的操作都设计相应的撤销结构,或是将错误处理和补偿的设计完全依赖流程设计人员。针对上述问题,我们提出了长事务补偿的设计和正确性保障途径。首先,从现有支持长事务的业务流程设计语言和理论研究中,抽象出了基于进程代数的长事务设计语言BaT。其次,给出了长事务补偿的设计准则,即在基于scope(域)的补偿和错误处理机制的层面上,保证在业务逻辑关键数据上,整个事务被提交或没有任何变更被提交(全做或不做准则),以及在父事务失败时,补偿保证恢复已提交的变更(补偿准则)。最后,给出了检验长事务补偿设计满足设计准则的充分条件——设计指导,并探讨了如何利用有界模型检验的方法验证业务流程中长事务补偿设计的正确性。