SaaS(Software as a Service,软件即服务),是随着互联网的飞速发展与应用软件的日趋成熟而形成的一种新型软件服务模式。它消除了企业购买、构建、维护基础设施和应用软件的需要,客户可以根据自己的实际需求,通过互联网获得厂商提供的服务。面向SaaS应用的典型特点是“单实例多租赁”,即多个租户共享服务提供商的一个应用实例,但对于每个租户来说,这个实例只像是为自己服务。然而这种统一的软件服务模式势必难以满足业务需求各异的不同租户,因此作为一个成功的SaaS应用,必须支持租户对其进行个性化定制,以便在共享实例的基础上构建专属于自己的业务应用。目前,面向SaaS的流程定制应用仍存在一些问题：首先,租户在定制过程中,无法保证行为活动的合理正确性,SaaS服务提供商的约束规范缺乏刚性；其次,难以满足租户对于服务的特殊定制；最后,租户的定制结果是由专门的业务流程编排语言(BPEL技术)将服务串联起来,而BPEL技术本身的静态特性,难以满足应用在执行过程中的动态改变。如果以上问题能够解决,将对SaaS应用的发展提供更为广阔的空间,因此有着重要的研究价值。针对SaaS业务流程定制中出现的主要问题,本文进行的主要工作包括：一、设计了规则驱动的SaaS定制及验证框架。该框架将规则的灵活性特点与传统BPEL技术的静态特性充分融合,实现了业务流程的灵活替换和动态修改,同时有效的提高了应用的处理能力,能够支持更为复杂的业务逻辑。二、提出了基于规则的服务封装机制。该机制引入规则的相关概念,通过包装和嵌入规则,能够允许租户对服务进行更为复杂的定制,以满足其实际业务需求,同时,解决了服务整合时接口不一致的难题,实现了不同服务对统一输入的有效接收。三、提出了基于TLA的流程定制验证算法。将活动时序逻辑与SaaS定制这两者有效的结合在一起,通过TLA公式建模的思想,将定制过程中的数据,流程,服务的状态形式化,并使用验证算法,对各个状态集合进行分析和矛盾检测,实现定制活动的正确性校验,有效的保证租户定制结果的合理可靠。本文提出了一个规则驱动的SaaS流程定制及验证技术框架。该框架独立于各种外部执行环境,具有较好的扩展性和可移植性,框架通过其中各个模块之间的相互协作,既能够实现租户的复杂定制,又能够对定制过程进行验证,而且在系统性能开销,功能执行和多租户支持方面表现良好,因此具有一定的可行性和可靠性。