化学抽象机.pptx

化学抽象机高旻建 王树锋 陈海潮化学抽象机CHAM基本概念LTS(带标号的迁移系统)LTS状态树生成算法应用：ATM的测试用例生成基本概念化学抽象机(CHAM)最早是由法国科学家 Gerard berry 和Gerard Boudol 提出来的，它主要用于异步并行计算模型的建模，通过把化学反应和抽象机的概念有机地结合来描述系统状态的变化。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，)S是溶液的集合，D是迁移规则集合， 是初始溶液，带标号的迁移系统(LTS)一个标号迁移系统是一个五元组是状态的集合，L是标号的集合， 是初始状态，是终止状态集合，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数组，Step2：如果 ,则终止，否则：Step2.1 对中的每一个分子进行检查，如属于自反应型分子，则进行重写操作(即发生反应)；同时构造反应树(状态树)；Step2.2 对中的每一对分子进行检查，如果匹配计算结果中的不为空，则将的值放入数组Reaction中；Step2.3 当数组Reaction不为空时，对非空的数组分量进行重写操作，以生成新的溶液，同时 构造反应树(状态树)；当数组Reaction为空时，返回Step2．LTS状态树生成算法?广义的LTS生成算法基于时间戳的思想并发控制问题每个分子的反应时都有确定的时间值，因此可以定义分子反应的先后次序，即前驱关系。1)如果a，b是两个分子，并且a在b之前被反应，则ab．2)如果a是提供数据分子，b是使用数据分子，则ab ．3)如果ab且b ，则a ．对数组Reaction的分量定义进行修正，在原有数据项的基础之上进行扩充，增加一个数据项timestamp表示每个分子的时间戳之值．LTS状态树生成算法(广义）串行化算法LTS状态树生成算法(广义）在修改算法1的基础上，使用算法2来生成一般的LTS状态