中文摘要：

SaaS模式已成为当前流行的软件服务形式.为满足不同租户个性化的业务服务需求,SaaS模式必须提供灵活的定制机制.为此,提出了一个支持租户业务流程定制行为建模及验证的框架.该框架以层次定制行为约束图作为定制指导,通过TLA（Temporal Logic of Actions）对各层的原子定制活动建模,并以此为基础构建租户的全局定制行为,然后基于应用的业务规则约束设计算法验证全局定制行为的正确性;为有效提高租户的定制效率,基于对多租户已有正确定制结果的统计分析,设计定制推荐算法,合理减少验证次数.仿真实验结果证实了该机制的高效性及可靠性.

英文摘要：

SaaS model has become a popular form of software services.In order to meet personalized business service needs of tenants,SaaS model must provide flexible business process customization mechanism.This paper proposes a modeling and verification framework for business process customization.Following the guidance of Hierarchical Customized Behavior and Dependency Graph,the framework models the atomic customization action based on TLA（Temporal Logic of Actions）,constructs the global customization behavior and designs the verification algorithm for tenants＇ global customization based on business rule constraints.Based on multi-tenants＇ feature and historical verified customization,this framework also constructs a customization recommendation algorithms to improve the efficiency of customization for tenants.Experiments demonstrate the efficiency and reliability of this customization and verification mechanism.