化学抽象机课件

化学抽象机高旻建王树锋陈海潮化学抽象机CHAM基本概念LTS(带标号的迁移系统)LTS状态树生成算法应用：ATM的测试用例生成基本概念化学抽象机(CHAM)最早是由法国科学家Gerardberry和GerardBoudol提出来的，它主要用于异步并行计算模型的建模，通过把化学反应和抽象机的概念有机地结合来描述系统状态的变化。CHAM在描述系统动态性、并行性方面的优良特性，因而可以较好地描述异步并行计算模型。CHAM形式化语义包括一组分子、溶液、变换规则。变换规则：从应用范围可分为通用规则和专用规则。从反应作用可分为：加热和冷却规则，反应规则结构一个化学抽象机由一组分子m0,m1,m2⋯、溶液s0,s1,s2⋯和变换规则组成分子是CHAM的基本元素,由一个常数集和操作符集派生而成的句法代数定义;溶液是由有限多个分子的集合,它反映了系统的某种状态,溶液中的分子根据变换规则进行反应化学抽象机规则变换规则从应用范围可分为通用规则,即在整个CHAM中通用的规则;专用规则,适用于某些特定分子的规则。从反应作用可分为加热规则,把大分子分解成小分子的规则;冷却规则,小分子合成大分子的规则从反应涉及的分子可分为自反应规则,只有单一分子的状态变化;互反应规则,反应过程中至少有两个分子参加反应化学抽象机膜结构的使用在CHAM中,膜是一种封装结构,任何溶液可以被看作一个关于其它溶液的单一分子,膜内的溶液可以独立进化。膜具有半可渗透性,允许某些分子进入和离开,通过膜上的气孔,可以有选择地从膜中抽取分子,同时,气孔的可逆性允许分子被重新吸收到原始溶液中,膜表示了复合构件,实际上提供了一种刻画系统模块化的途径化学抽象机化学抽象机的优势与其他以状态机为转换模型的技术相比,CHAM利用化学反应这一隐喻,因此在刻画系统的动态性特征方面比较自然CHAM规格说明是一个基于操作的系统框架,这种框架不会把所描述的系统曲解为某种特定的计算模型CHAM描述不仅可以描述系统静态特征,还能从系统操作动态性方面进行描述,通过对各单元的描述、引入的转换规则及项重写描述和分析体系结构的动态行为,因而可使软件开发人员很快地了解系统功能和行为,适用于多种层次的用户能够有效地描述体系结构的动态特性，并且其动态特征能够用LTS表示出来，这为体系结构测试提供了基础．因此生成LTS是基于SA规格说明测试的关键问题．化学抽象机LTS状态树生成算法狭义的LTS生成算法（算法1）基于自反应和偶反应的LTS规则和溶液的数据结构用广义表表示。广义表是线性表的推广，它的每个分量可以是一个元素或一个广义表主要操作：Head(L),Tail(L),Replace(L1,L2),Match(L1,L2,Tk)还有一个数组Reaction，其分量是广义表，用于存储将发生反应的溶液分子以及反应规则。

LTS状态树生成算法

LTS状态树生成算法(广义）在修改算法1的基础上，使用算法2来生成一般的LTS状态树应用：ATM测试用例生成精简的ATM状态图应用：ATM测试用例生成构造CHAM的形式应用：ATM测试用例生成初始溶液的定义L

P

A:A代表P处理之前用户/系统已经完成的操作，L代表P处理之后才会发出的操作。应用：ATM测试用例生成终止溶液应用：ATM测试用例生成定义反应规则应用