一. 张敬周，任洪敏，宗宇伟，钱乐秋，朱三元. 基于行为自动机的构件可替换性分析与验证. 软件学报，2010，21（11）：2768-2781.
Time：1 hour
略读了同事的论文，本文关于构件的可替换性分析，结合有限状态自动机理论，用形式化方法给出了构件、构件行为、替换等一些列定义和定理，没有详细阅读。定义数学味很浓，用数学描述了相关问题，但定理没有给出证明过程，给出的行为可替换性验证算法也稍显简单（也许就该这么简单）。最后用购书做了实例分析（就是把定义用例子形象说明了一下）。
这类论文大多用数学理论说明某个问题，给出该问题的形式化定义，基于这些定义给出几个定理并证明之，再给出几个算法，然后用一个实际生活中的例子形象说明一下。还要把相关国际国内研究工作现状简单说明一下。
名词解释：
有限状态自动机（nondeterministic finite automata），详见《离散数学》。
二．沈洁，赵培欣，张亮，施伯乐. 一种增强Web服务可信度的代表元一复件模型. 计算机研究与发展. 2007，44(Suppl.)：35-39.
TIme：0.5 hour
摘录以上两个定义。
三. 陈振邦，王戟，董威，齐治昌. 面向服务软件体系结构的接口模型. 软件学报. 2006，17（6）：1459-1469
Time：0.5 hour
摘录：
定理1．对于SI，CI和PI，相容的组合操作都是可交换和可组合的．
在系统设计或运行过程中，可能会用某个服务替换系统中的另一个服务，并且希望替换后的系统仍然能够正常运行．对于服务的接口，我们认为它的本地动作及其类型是这个服务对于外界环境的保证，而必需动作是对外界环境的假设．如果新服务所提供的保证不比原来的服务少，而对外界环境的假设不会更多，我们就认为新的服务对于原来的服务是可以替换的．
四.邓水光，李莹，吴健，邝砾，吴朝晖. Web服务行为兼容性的判定与计算. 软件学报. 2007，18（12）：3001-3014
Time：1 hour
本文用形式化方法给出了服务行为兼容性定性和定量判定的计算方法和算法，用这种方法可以为服务替换提供帮助，保证服务替换的正确性和可用性，并能找到最佳的服务。
摘录整理：
服务行为兼容性的判定引起了国内外学者的关注。但这些工作大多基于Petri网(如文献[3])、有限状态机(如文献[5])或者自动机理论(如文献[8])展开。一旦服务行为、服务间的交互过程变得错综复杂时，这些方法都将出现空间爆炸，从而导致计算和判定的复杂度增大。此外，这些方法均只实现兼容性的定性判定。
基于Petri网、有限状态机和自动机的方法在服务行为的描述上采用图形方式较为直观．但当服务行为和服务问的交互过程变得较为复杂时，这种图形刻画的方式容易出现状态空间爆炸，其计算、验证和判定的复杂度也随即增加。因此，有研究人员提出采用进程代数的方法(如通信系统演算CCS、通信顺序进程CSP和
演算)来刻画服务行为和服务之间的交互。
五．胡昊，殷琴，吕建．虚拟计算环境中服务行为与质量的一致性．软件学报．2007，18(8)：1943-1957
Time：1 hour
本文中基于petri网理论，对服务行为等进行形式化定义。
Ebert 和 Engles 对调用一致性和观察一致性给出了如下解释:
调用一致性给出了子类提供行为的下限(lower bound),即在一个超类中可被调用的任何行为序列都能够在子类中被调用；
观察一致性给出了子类提供行为的上限(upper bound),即任何从子类可观察到的行为经过投影映射后都应当与超类的可观察行为对应；
van der Aalst 也给出了另一种角度不同但意义相同的解释,当子类中新增的行为被阻塞(block)时,其保 留的行为与超类行为一致,则称为协议一致性;而当子类中新增的行为被隐藏(hide)时,其保留的行为与超类行为一致,则称为投影一致性。van der Aalst 特别指出协议一致性与调用一致性概念相同,而观察一致性与投影一致性概念相同。