随着SO A、Web服务技术的发展,越来越多的软件系统采用SOA的架构来实现,这类系统称为基于服务的软件系统。基于服务的软件系统面向用户需求变化或系统环境变化时,对系统的组成和结构进行动态调整,不断进行演化实现系统优化,从而具有自适应的能力,称作是自适应的基于服务的软件系统(Adaptive Service Based System, ASBS)。ASBS系统在生命周期中不断进行调整和变化,采用形式化验证技术对ASBS系统进行模拟和分析是保障演化的ASBS可靠执行的一种有效途径。目前,学术界和工业界从不同侧面展开了对ASBS系统的研究工作,已有大量研究成果,但还存在以下问题：基于何种形式化模型来模拟ASBS系统的动态演化,对不断变化的系统进行建模和分析；如何定义ASBS调节时的演化策略,使得演化策略能够灵活的适用于不同的演化场景；在面向离线演化时,如何判定演化策略执行的结果是否保持系统的流程一致性；在面向在线演化时,基于什么样的标准能够判定调节时的替换策略能否正常执行。由于ASBS系统具有自适应的特性,对ASBS系统进行验证分析的形式化工具需要考虑系统不断进行变化和调整的特征。本文基于反射Petri网模型,提出了有色反射Petri模型,从系统本身和变化两方面分别对ASBS系统建模；从ASBS系统在线演化和离线演化两个不同层面定义和描述演化策略,提出演化策略生成算法；针对系统离线演化时流程能否保持一致的问题,分别从控制流和数据流两方面,提出流程一致性的分析和判定方法；针对在线演化时服务依据哪种标准进行有效替换的问题,提出基于行为效果的服务可替换性分析和判定方法。本文在以下方面开展了工作。(1)针对ASBS系统动态演化特性的建模问题,建立有色反射Petri网模型,基于有色反射Petri网构建ASBS演化模型。根据ASBS需要动态适应外部变化、自动进行调整的特性,本文提出使用反射Petri网模型对系统本身和变化部分分开进行建模,充分表达ASBS系统的自适应特性。但反射Petri网的基层模型在表示组合服务的语义信息方面不足,本文扩展现有的反射Petri网模型,给出有色反射Petri网模型,基于有色反射Petri网模型对ASBS系统进行建模,描述具体的建模过程,为ASBS系统的验证和分析奠定基础。本文结合在线购物系统建模的具体实例,证明有色反射Petri网模型可以有效的支持ASBS系统的建模。(2)针对不同演化场景的演化策略表示问题,提出面向在线和离线演化的两种演化策略表示模型,针对离线演化的调整动作定义问题,提出ASBS演化策略的生成算法。ASBS系统处于一个不断变化的环境中,一方面需要对外界环境的变化做出响应进行在线的实时调整,另一方面系统需要面向用户需求和系统设计方面的变化进行离线的流程结构调整。为了能够支持ASBS面向不同变化进行调整的场景,本文提出从在线和离线两个层面定义面向服务替换和面向流程重构的演化策略。当ASBS进行流程重构时,在用户定义好变化前后的流程描述文档情况下,本文提出基于图编辑距离的思想实现演化策略生成算法,通过具体的实例说明算法是正确的、有效的。(3)针对离线演化时的流程一致性问题,基于有色反射Petri网模型提出ASBS系统的流程一致性分析和判定方法。当ASBS系统运行到一个阶段,为了满足新的业务需求,系统会执行离线的演化策略进行重配置,在重配置的过程中,如何保证系统正常执行,需要对演化过程中系统的流程一致性进行分析和验证。本文提出基于有色反射Petri网模型、从控制流和数据流两方面对ASBS系统的流程一致性进行判定。控制流一致性判定主要对流程结构进行分析,如无死锁、死变迁等,数据流一致性判定主要对流程中活动之间的数据依赖关系进行分析,针对流程中的数据冗余、数据不匹配等问题提出判定方法,二者相结合实现了面向离线演化时的ASBS系统流程一致性分析。(4)针对在线演化时的服务可替换性问题,提出基于行为效果的服务可替换性分析和判定方法。ASBS进行在线的动态调整时,如果网络中出现了一个新服务或者正在执行过程某一个服务不好用,需要进行服务的动态替换。进行服务无缝集成与协作中一个重要问题是对服务可替换性的分析,在基于行为的服务组合场景下,考虑基于行为效果的服务可替换性定量判定方法,通过定义服务行为模型、服务行为效果、行为效果一致和服务可替换度,结合Petri网变换理论计算服务可替换度,实现基于行为效果的服务可替换性分析。