化学抽象机

化学抽象机高旻建王树锋陈海潮化学抽象机CHAM基本概念LTS(带标号的迁移系统)LTS状态树生成算法应用：ATM的测试用例生成基本概念化学抽象机(CHAM)最早是由法国科学家Gerardberry和GerardBoudol提出来的，它主要用于异步并行计算模型的建模，通过把化学反应和抽象机的概念有机地结合来描述系统状态的变化。CHAM在描述系统动态性、并行性方面的优良特性，因而可以较好地描述异步并行计算模型。CHAM形式化语义包括一组分子、溶液、变换规则。变换规则：从应用范围可分为通用规则和专用规则。从反应作用可分为：加热和冷却规则，反应规则基本概念用CHAM描述的软件体系结构规格说明包括四个部分：1、体系结构组成构件（即分子）的语法描述，构件分为3类：数据元素、处理元素和连接元素2、系统的初始状态（即溶液S。）3、一套反应规则4、一组表示系统状态变化的溶液集结构一个化学抽象机由一组分子m0,m1,m2⋯、溶液s0,s1,s2⋯和变换规则组成分子是CHAM的基本元素,由一个常数集和操作符集派生而成的句法代数定义;溶液是由有限多个分子的集合,它反映了系统的某种状态,溶液中的分子根据变换规则进行反应化学抽象机规则变换规则从应用范围可分为通用规则,即在整个CHAM中通用的规则;专用规则,适用于某些特定分子的规则。从反应作用可分为加热规则,把大分子分解成小分子的规则;冷却规则,小分子合成大分子的规则从反应涉及的分子可分为自反应规则,只有单一分子的状态变化;互反应规则,反应过程中至少有两个分子参加反应化学抽象机膜结构的使用在CHAM中,膜是一种封装结构,任何溶液可以被看作一个关于其它溶液的单一分子,膜内的溶液可以独立进化。膜具有半可渗透性,允许某些分子进入和离开,通过膜上的气孔,可以有选择地从膜中抽取分子,同时,气孔的可逆性允许分子被重新吸收到原始溶液中,膜表示了复合构件,实际上提供了一种刻画系统模块化的途径化学抽象机化学抽象机的优势与其他以状态机为转换模型的技术相比,CHAM利用化学反应这一隐喻,因此在刻画系统的动态性特征方面比较自然CHAM规格说明是一个基于操作的系统框架,这种框架不会把所描述的系统曲解为某种特定的计算模型CHAM描述不仅可以描述系统静态特征,还能从系统操作动态性方面进行描述,通过对各单元的描述、引入的转换规则及项重写描述和分析体系结构的动态行为,因而可使软件开发人员很快地了解系统功能和行为,适用于多种层次的用户能够有效地描述体系结构的动态特性，并且其动态特征能够用LTS表示出来，这为体系结构测试提供了基础．因此生成LTS是基于SA规格说明测试的关键问题．化学抽象机LTS:带标号的迁移系统迁移系统(TS)一个迁移系统T是一个三元组(S，D，s0)S是溶液的集合，D是迁移规则集合，s0∈𝑆是初始溶液，带标号的迁移系统(LTS)一个标号迁移系统是一个五元组𝑆,𝐿,𝑆0,𝑆𝐹,𝑇𝑆是状态的集合，L是标号的集合，S0∈𝑆是初始状态，𝑆𝐹是终止状态集合，T是迁移关系LTS与CHAM之间的关系是LTS作为CHAM的动态性表示。LTS状态树生成算法狭义的LTS生成算法（算法1）基于自反应和偶反应的LTS规则和溶液的数据结构用广义表表示。广义表是线性表的推广，它的每个分量可以是一个元素或一个广义表主要操作：Head(L),Tail(L),Replace(L1,L2),Match(L1,L2,Tk)还有一个数组Reaction，其分量是广义表，用于存储将发生反应的溶液分子以及反应规则。LTS状态树生成算法算法1步骤Step1：初始化Reaction数组，𝑆0,𝑆1Step2：如果𝑆0=𝑆1,则终止，否则：Step2.1对𝑆0中的每一个分子𝐶𝑖(𝑖=1……𝑛)进行检查，如𝐶𝑖属于自反应型分子，则𝐶𝑖进行重写操作(即发生反应)；同时构造反应树(状态树)；Step2.2对𝑆0中的每一对分子𝐶𝑖,𝐶𝑗(𝑖,𝑗=1⋯𝑛)进行M𝑎𝑡𝑐ℎ(𝐶𝑖,𝐶𝑗,𝑇𝑘)检查，如果匹配计算结果中的𝑇𝑘不为空，则将𝐶𝑖,𝐶𝑗,𝑇𝑘的值放入数组Reaction中；Step2.3当数组Reaction不为空时，对非空的数组分量进行重写操作，以生成新的溶液𝑆0，同时构造反应树(状态树)；当数组Reaction为空时，返回Step2．LTS状态树生成算法广义的LTS生成算法基于时间戳的思想并发控制问题每个分子的反应时都有确定的时间值，因此可以定义分子反应的先后次序，即前驱关系。1)如果a，b是两个分子，并且a在b之前被反应，则a→b．2)如果a是提供数据分子，b是使用数据分子，则a→b．3)如果a→b且b→c，则a→c．对数组Reaction的分量定义进行修正，在原有数据项的基础之上进行扩充，增加一个数据项timestamp表示每个分子的时间戳之值．LTS状态树生成算法(广义）串行化算法LTS状态树生成算法(广义）在修改算法1的基础上，使用算法2来生成一般的LTS状态树应用：ATM测试用例生成精简的ATM状态图应用：ATM测试用例生成构造CHAM的形式应用：ATM测试用例生成初始溶液的定义L◇P◇A:A代表P处理之前用户/系统已经完成的操作，L代表P处理之后才会发出的操作。应用：ATM测试用例生成终止溶液应用：ATM测试用例生成终止溶液应用：ATM测试用例生成定义反应规则应用：ATM测试用例生成定义反应规则应用：ATM测试用例生成定义反应规则应用：ATM测试用例生成CHAM导出LTS应用：ATM测试用例生成CHAM导出LTS应用：ATM测试用例生成迁移覆盖测试序列化学抽象机谢谢！