论文阅读和写作暂停了半年时间，新房装修、结婚、搬家…一系列事情总算忙完了。重新开工。
一．史玉良，王海洋，张亮，施伯乐. web服务合成的相容性与替换性分析. 计算机研究与发展，2007，44(11)：1955～1961．
本文用自动机进行形式化描述和建模，对相容性和替换性做了定义和分析。
二．刘方方，史玉良，张亮，施伯乐．基于进程代数的web服务合成的替换分析. 计算机学报，2007，30（11）：2033-2039.
Time：2.5 hours
本文提供了一种基于进程代数的web服务替换方法。文章首先给出web服务合成的正确性描述，然后给出上下文无关的概念（即提出一种一致性关系），在这两者的前提下，即可完成web服务替换工作。
文中1，2两部分简要介绍了web服务合成和替换，以及两者的研究现状。
第3部分先指出文献[1]中两处不足：
1. 研究前提是消息同步传递，未考虑消息异步传递。因为异步消息传送时，调用者在发送消息后无须等待，可以接着处理其他任务。这样可能造成别的服务消息提前到达，超过存活期后失效，从而造成合成失败。
2.对于合成正确性的描述提出的subtype关系考虑不全面，只考虑了全局选择分支，未考虑内部选择。（个人并不是非常认同，文献[1]的作者应该不会犯这么低级的错误，若要写这个方面的论文，需精读文献[1]验证）。
接着本文基于进程代数给出了web服务正确性和一致性的形式化定义，提出一种一致性关系的定理，并用反证法证明，最后简单写了一个判断两个由CCS过程描述的Web服务是否存在一致性关系的算法。
从此论文来看，写论文也不是件太难的事情。
名词解释：
进程代数（Process Algebra）的一个显著特征是把并发性归结为非确定性，将并发执行的进程的行为看成是各单个进程的行为的所有可能的交错合成，即所谓交错语义。进程代数研究的核心问题是进程的等价性，即在什么意义下两个进程的行为相同？在进程代数领域使用的最为广泛的等价关系有互模拟、测试等价、失败等价(参见通信顺序进程)等。对这些语义等价关系均建立了相应的公理系统。关于公理系统的研究不仅加深了对语义理论的理解，而且使得有可能对语义等价关系进行形式推理。
CCS（Communication and Concurrency System）。
三．刘莹，张一川，张斌，张明卫，朱志良．基于行为效果的服务可替换性分析．计算机研究与发展，2010，47（8）：1442-1449.
Time：3 hours
本文先说明现有服务替换形式化方法的某种不足之处，然后基于某种成熟理论，提出一种新的分析方法：给出数学定义、可具体量化的度量参数，然后说明如何通过算法得到这些参数。这种写论文的思路要借鉴学习。
本文提出了一种基于行为效果的可替换性分析方法，该方法描述基于行为的服务模型，采用有色Petri网对服务行为建模，利用服务内部的触发事件、结果事件间的关系分析行为效果，给出了基于行为效果的服务可替换度的概念，结合规则对可替换的目标进行证明，基于有色Petri网的服务行为模型，提出实现服务可替换度的计算方法。
0 引言部分
在形式化验证中对服务可替换性的分析也有两种不同方式，一种是面向服务功能，以操作为粒度对服务可替换性进行验证。另一种是面向服务行为，以业务服务(业务活动)为粒度的服务可替换性验证。
目前，基于行为的服务替换研究主要集中在被替换服务和候选服务执行时内部操作序列的匹配方面。基于内部操作序列一致性的替换性分析方法必将减小替换服务的候选空间，导致有效的替换服务被忽略。
本文认为可以将行为效果的等价性作为判定两个服务是否可替换的重要依据，从而提出了本文的观点。
1 ，2 正文部分
本文以“旅行计划”的组合业务为例，采用有色Petri网理论，给出了服务执行一次操作的活动、服务行为模型、服务行为效果、运算符
、服务行为效果一致、可替换度（证明了一个定理）、替换效果的数学定义，通过形式化方法来描述这些感性的词汇，包括几个度量参数。
基于以上，提出基于Petri网的服务可替换度计算方法，给出3个具体的算法，可以得到本文定义的度量参数，以便定量的计算服务的可替换度。
3 相关研究
自动机理论、有限状态机和Petri网是对服务行为的可替换性研究的是使用最多的形式化分析方法，本节做了简单介绍，因为是本文研究工作的基础，包括服务行为建模方法等。
名词解释：
有色Petri网（着色Petri网，Colored Petri Net，CPN）:
一种对标记分类以实现网系统折叠的高级Petri网。由于普通Petri网没有数据的概念，所有的数据控制必须转化为网结构，导致模型非常庞大。CPN引入了数据类型和数据操作的概念，使网系统中的基本元素减少，从而缩小网系统的规模，同时还增强其表达能力更强，使得模型清晰且易于理解。
CPN具有以下特点，首先，CPN继承了Petri网图形表示、模型直观易懂的特点。CPN是对Petri网系统的一种折叠和抽象，对于每个CPN都可以构造出一个与之行为
等价的Petri网系统，只不过对应的库所Petri网系统会包含更多的基本元素。另外，为了更清晰的描述复杂系统，CPN提供了层次化建模的方法，通过关联更小的CPN
模型的方式来构造更大CPN模型，这类似于程序设计语言中使用程序模块或者子程序的思想。
CPN提供的验证方法有四类：构造可达图、计算并解释系统不变量、化简以及检测结构属性。其中前两种是主要的验证方法。
CPN是一种形式化系统模型，可以用来描述、分析以及验证离散事件动态系统。CPN 结合了Petri 网图形表示的优点和编程语言处理数据的优势，适合对大型复杂系统进行分析与评价。
四. 印莹，张斌，张锡哲．面向组合服务动态自适应的事务级主动伺机服务替换算法．计算机学报，2010，33（11）：2147-2162.
Time：3 hours
本文将事务加入服务替换中，引入数学模型成文，最后本文提供了实验结果，比较难得。暂不精读本文，有需要用到事务时再来阅读。
摘录：
现有服务替换机制大多缺乏事务支持，本文解决了三个问题：事务级服务替换范围识别，事务级服务替换QoS代价/收益模型，高效替换算法。
传统替换机制大多采用备份服务或者服务路径直接替换。
采用锁定资源的策略，如严格二阶段提交机制(2PC) 不再适用，而是有选择地放松事务对ACID性质的要求，并引入补偿机制，用以消除已经执行的Web服务对系统的影响(比如释放空间等)。
由以上分析可知，在服务运行过程中，当已经提交的事务需要被替换时，为了维护事务的原子性和数据的一致性，需要知道事务粒度及补偿范围．
如何快速识别事务粒度及替换范围来维护替换前后数据的一致性问题是实现正确替换的首要问题；另外，设计一个能够反映补偿支持的服务替换代价／收益模型成为替换过程的重要问题；最后，如何快速发现失效服务并响应替换，减少中断时间，提高替换时效性是事务级替换要解决的另一个重要问题．
目前的替换模型有两种方式：面向功能的替换和面向组合服务QoS的替换。
五。李喜彤，范玉顺．Web服务流程相容性和相似性分析．计算机学报，2009，32（12）：2429-2437.
本文基于着色Petri网建模Web服务流程，给出服务流程相容性、相似性的定义，然后给出相应判定算法。要先学习Petri网的基础理论，然后再阅读。