形式化CHAM语言的软件设计辅助工具

摘要：化学抽象机（Chemical Abstract Machine）是由Berry和Boudol在1990年提出的用于异步并行计算建模的模型，它借用化学反应的隐喻，通过化学中分子和化学反应的概念和抽象机模型的特点来描述系统状态的动态变化，但复杂的形式和缺乏工具支持限制了它的使用。本文以上知识的基础上编写的一款CHAM化学抽象机形式化语言书写支持工具，用来支持CHAM的设计工具。本文对工具的界面和程序和功能进行介绍，在此基础上，分析此工具的优缺点，并给出改进的方法和方向。

关键词：统一建模语言；化学抽象机；状态图；形式化

中图分类号：TP301文献标识码：A文章编号：1007-9599 (2011) 08-0000-00

Software Design Assistant-Tool of Formalization CHAM Language

Cui Gengdi1,Cui Guangji2

(1.Jining University,Jining273155,China;2.College of Computer Science and Technology,Taiyuan University of Technology,Taiyuan030024,China)

Abstract:Chemical Abstract Machine designed by Berry and Boudol in 1990 was used for asynchronous parallel computing,which borrows the metaphor of chemical reactions.The CHAM model descript the system changes though molecular and chemical reactions in the concept and characteristics of the abstract machine model.But the complexity and lack of tool support in the form of restricted its use.On the basis of knowledge of chemical abstract machine.We design a writing support tools using formalization CHAM language to support the CHAM language.In this paper,interfaces and functions will be introduced in this paper.Then,the analysis of advantages and disadvantages of this tool will be introduced,and give an improved method and direction at last.

Keywords:UML;CHAM;Statecharts;Formalization

一、简介

化学抽象机[1]简称CHAM（chemical abstract machine）最初用来给出π演算的操作语义，化学抽象机是由Banatre和Le Metayer的Γ语言发展而来，借用了化学隐喻，为描述并行计算提供了形式化框架。[2]

化学抽象机模型是系统的单个状态看成是一个溶液（Solution），通过溶液之间变化的化学反应来描述系统的动态变化。在这个模型中，溶液的变化是由组成溶液的分子（Molecule）来体现的，在保证反应规则的分子集不重叠的基础上，溶液之间的分子可以按照反应规则各自并行的进行反应。

本质上，CHAM可看成一种有限状态机，它具有一般状态机特征，与其他以状态机为转换模型的技术相比，CHAM利用化学反应这一隐喻，因此在刻画系统的动态性特征方面比传统形式化语言方便。CHAM规格说明是一个基于操作的系统框架，这种框架不会把所描述的系统曲解为某种特定的计算模型。CHAM描述不仅可以描述系统静态特性，还能对系统动态性方面进行描述，通过对各单元的描述、引入的转换规则及项重写描述和分析体系结构的动态行为，因而可使软件开发人员很快地了解系统功能和行为，适用于多种层次的用户。CHAM定义了两种用于描述的结构――膜和气孔。膜是半透性的封装结构，有选择的允许分子的进出，膜内的溶液可以独立进化，气孔是一种可逆性结构，允许分子无条件地被重新吸收到原始溶液中。

二、规格和描述说明

本文在文章[3]，[4]的基础上，总结了一种可以普遍使用并具有代表性的形式，并结合系统状态的特点，将状态图形式化[5]后具有的性质添加进入，这些内容能够体现辅助工具的设计思想。

（一）规格说明

M：：=ST|E|G|B|MM

ST：：=States（InternalVariables）|InitialState|FinalState

E：：=Transform_Event|InternalAction

C：：=Event?（E）|Event!（E）|Level_Message?（E）|Level_Message!（E）

这是一种使用化学抽象机模型对系统状态的定义方法，由于篇幅关系，对这种定义的研究方式不在叙述，只是解释相关的概念。其中，状态元素ST包含三种状态，一种是状态可能包含内部变量的正常状态，另外两个分别是初始和结束状态，事件元素E这里分为两种，一种是可以改变事件Transform_Event；一种只能改变内部变量的事件InternalAction，使用在进程通讯系统中使用的符号“?”（输入）和“!”（输出）来表示迁移的方向，Event和Level_Message来表示两种类型的信息，分别是普通迁移和层次化信息。

（二）初始溶液形式

S1=InitialStateEvent!（E1），

Event?（E1）Event!（E2）States（a1），

……，

Event?（E（n-1））Event!（E（n））States（a（n-1）），

Event!（E（n））Level_Message!（Ex1）States（a（n-1）），

Level_Message?（Ex1）States（a（n））_InitialState，

…….，

Event?（E（n+m））FinalState；

（三）反应规则形式

T1=InitialStateEvent!（E）Event!（E）InitialState（加热反应规则）

T2=Event!（E1）ST1，Event?（E1）Event!（E2）ST2ST1Event!（E1），Event!（E2）ST2Event?（E1） （化学反应A规则）

T3=Level_Message!（E）ST1，Level_Message?（E）Event!（E1）ST2_InitialStateST1Level_Message!（E），Event!（E1）ST2Level_Message?（E） （化学反应B规则）

三、软件设计辅助工具的设计

（一）辅助工具的界面介绍

如图1所示，这是一种化学抽象机形式化语言的书写支持工具，用于对使用CHAM进行软件设计的支持，软件提供了一些常用按钮、溶液检查功能、规则检查功能和溶液的自动生成功能。

图1 工具界面

界面下方是化学抽象机形式化语言目前可以使用到符号或者字符串，其中常用符号可以用于判断和检查。由于文本框的原因，“”和“”无法输入，改为“”和“―〉”两种类似符号，便于输入和处理，此类按键的设计思想来源于Z-EVES工具，目的是为了方便用户书写和避免相似符号造成不必要的错误。某些按键现在无法用到，如保护键，但为了软件的进一步改进，仍将其放在此处。

软件中含有三个功能按钮，初始溶液检查按钮、规则检查按钮和溶液生成按钮。初始溶液检查按钮和反应规则检查按钮是为了对使用者在书写化学抽象机形式化语言时，由于语言形式繁琐而可能出现的错误，本文可以按照事先设置的规则对初始溶液和规则进行检测。溶液生成按钮可以让使用者通过初始溶液和规则的输入来生成下一步的溶液，简化书写的步骤。

（二）功能及算法介绍

1.初始溶液检查按钮

初始溶液的内容设置在本文框Solution中输入，输入的所有内容都当作字符或字符串处理，对初始溶液的检查基于输入/输出守恒的思想，由于化学抽象机形式化语言的特殊性，在描述状态图时用到的CHAM语言中初始溶液的形式具有以下特点：

初始溶液的内容设置在本文框Solution中输入，输入的所有内容都当作字符或字符串处理，对初始溶液的检查基于输入/输出守恒的思想，由于化学抽象机形式化语言的特殊性，在描述状态图时用到的CHAM语言中初始溶液的形式具有以下特点：

（1）初始溶液不能为空；

（2）在初始溶液中出现的“{”，“|”，“/”符号不会当作有意义的符号处理，减少因为格式的限定而出现的错误；

（3）初始溶液的第一个分子以字符串“States”开始；

（4）第二个到以后的分子必须以字符串“Event?”或者“Level_Message?”开始；

（5）“Event?”字符串出现的次数必须和“Event!”字符串出现的次数相同，“Level_Message?”字符串出现的次数必须和“Level_Message！”字符串出现的次数相同。

CHAM书写工具会返回错误的类型和地方，将它返回到ErrorCheck文本框中，需要说明的是：第一、这仅是一种书写工具，提示的错误只提供一种参考作用，允许使用者保留原有形式并执行之后的操作；第二、使用上述规则对代表系统设计的初始溶液进行检查，前提是设计者使用了CHAM形式化语言这种形式，可以看到，错误的检查的基础是牺牲了形式的灵活性。

2.输入规则的检查

规则的处理思想是基于反应前后分子形式变化的特点，对于规则的检查基于如下四条：

（1）“反应规则”中，字符串“”之前的内容和字符串“”之后的内容不能相同，即形如“TiABCDEFGHIABCDEFGHI”是不被允许的。

（2）“反应规则”中，任意两个反应规则不能重复，即：“TiABCDEFGHIDEFABCGHI，TjABCDEFGHIDEFABCGHI （i≠j）”是不被允许的。

（3）“反应规则”中，反应之前的分子中的“离子”的个数和种类在反应之后能保持不变，即“”之前的字符串中，每个“”之前和之间字符串必须在“”之后的字符串中也能找到，例如：TiABCDEFGHIDEFABCGHI中，“”之前有ABC，“”之后也要有ABC。

（4）反应规则不能为空。在此工具种对于反应规则的检查，只限于对形式的检查，而不涉及内容，这是因为可以使用溶液来检查内容，没有必须通过反应规则再对内容做检查，具有错误内容的反应规则，无法通过溶液的自动生成功能生成新的溶液。

（三）溶液的自动生成

为了简化书写，软件提供溶液的自动生成功能，即在已有溶液的基础上，通过使用者选择的反应规则，自动输出溶液。由于笔者能力和时间所限，只能涉及三种规则，分别是加热规则、反应规则和打散规则，软件可以在对使用者输入规则类型进行判断的基础上，处理溶液，并自动生成溶液，如果无法生成，会提示错误信息。

需要说明的是，此软件本身只是一种书写工具，对正确性的要求并不苛刻，所谓的反应规则检查和初始溶液检查功能虽然可以检查和显示不符合软件规定的形式，但只是像Microsoft Word当中的对错误的字和不符合语法的句子使用下划线功能那样提供一种提示功能，如果使用者无视提示的错误，软件仍然会提供溶液的自动生成功能。

（四）部分使用的函数及变量

BOOLEmptySolutionText（） //判断溶液文本框中的内容是否为空

INTSkipSpecialChar（） //跳过特殊符号 如{、/、|，Return 0

INTNumberofMolecu（） //返回溶液中分子的序号

INTTheFirstMolecu.FIND （“States”）//找到第一个分子中States字符串的位置

INT TheRemainingMolecu.FIND （“Event?”） //找到从第二个分子开始的分子中“Event?” 字符串的位置

BOOLEvent_NeedFind；//判断Event?字符串是否需要继续查找

INTTheRemainingMolecu.FIND （“Event?”） //找到从第二个分子开始的分子中“Event?” 字符串的位置

BOOLL_M_NeedFind；//判断字符串是否需要继续查找

INT GetCountChar （string Solution，“Event?”） // 得到溶液中Event？字符串的数量

INTGetCountChar （string Solution，“Event!”）

INTGetCountChar （string Solution，“Level_Message?”）

INTGetCountChar （string Solution，“Level_Message!”） //以上为溶液检查中用到的函数；

BOOLEmptyRulesText（） //判断反应规则文本框中的内容是否为空

pare （） //用于比较反应规则，返回是否为相同规则的函数

pare（EndReaction） //用于比较反应前后的分子是否相同的函数

pare （） //比较离子的函数

BOOL EmptyNumberofRules（） //是否有反应规则的序列号，输入类型为SelectNumber=int n；

INTTypeofRules（） //判断反应规则的种类

四、辅助工具的功能测试与结果

图2 规则检查结果

列举两个错误初始溶液的检查结果，分别为测试用例3和测试用例7：

图3 溶液的检查结果

使用测试用例6中的初始溶液作为溶液生成的演示，在自动生成之前，进行溶液正确性检查：

图4 溶液的检查结果

上面的示例中为了完整的显示整个初始溶液，所以在Level_Message?之后加入了换行，但在实际中是不允许的，系统设定加入换行输入SelectNumber=int n；之后，系统将对n的值进行检查，找到匹配的规则进行替换。如下图所示：

（a）

（b）

图5 溶液的生成

五、测试结果分析

目前工具存在很多不足，软件本身的稳定性存在问题，存在多次修改错误的反应规则后，使用规则检查功能可能将正确的规则显示为错误的可能性；由于规则检查功能和溶液自动生成功能规定方法的局限性，实际上，通用规则无法正确的在溶液生成中得到使用。另外，可以注意到CHAM形式化语言中规格说明被没有在工具中使用。这种规格说明可以用来判断状态、时间和层次化信息的正确性，由于作者能力所限，并没有设计这项功能所需规则。

工具检测的错误检测建立在化学抽象机复杂形式的基础上，形式化语言对于书写的格式要求苛刻，描述的方式需使用者熟悉各种规则，笔者考虑一种从用来描述UML视图的工具Rational Rose的MDL文件中提取信息并转换为化学抽象机形式化语言的方式，对于UML中由于形式的灵活性造成的二义性和模糊性，使用提示的方法让用户去选择，这种方法有效地减少用户的工作量，并结合了图形化描述方式的灵活性和形式化语言的精确性。

六、结论与展望

此书写工具有如下优点：

（一）自动检测的方法保证形式的正确性；

（二）使用溶液自动生成的方法减少人工书写的复杂性

（三）使用添加经常使用的字符和字符串的方式提高书写的效率

书写工具实现了一些基本功能，但对于一个成熟的工具来说，这是远远不够的。比如工具并没有涉及所有的溶液和反应规则，而且只是降低了书写的难度，仍然需要使用者对化学抽象机语言有一定的了解才可以使用，今后需要在各个方面添加和完善功能。

参考文献：

[1]Berry G,Boudol G.The Chemical Abstract Machine[J].Theoretical Computer Science,1992,96:217-248

[2]P.Inverardi,A.L Wolf.Formal Specifications and Analysis of Software Architectures Using the Chemical Abstract Machine Model[J].IEEE Transactions on Software Engineering,1995,21(4):373-386

[3]赵良,叶俊民.基于CHAM描述的类簇级测试用例生成方法研究[M].武汉:华中师范大学,2005

[4]Apostolos Syropoulos.Fuzzy Chemical Abstract Machine[J].Lecture Notes in Computer Science,2009,20

[5]SUN Meng ZHANG naixiao.The Formalization for UML Statecharts Diagrams[J].Acta Scientiarum Naturalium Universitatis Pekinensis,2005,41(3):103-115

[作者简介]崔耕第（1960-），男，济宁学院计算机系，副教授，研究方向为计算机网络软件与应用。近年来，主持并参与省市级科研项目《基于IEEE1588的电力系统时间同步技术研究》《基于互联网行为的IPv4/IPv6网络测量应用研究》等课题4项，精品课程2项；崔光霁（1983-）：男，太原理工大学计算机科学与技术学院，硕士，研究方向为形式化语言与软件测试。

“本文中所涉及到的图表、公式、注解等请以PDF格式阅读”