计算机应用   2017, Vol. 7 Issue (2): 574-580  DOI: 10.11772/j.issn.1001-9081.2017.02.0574
0

引用本文 

李雪, 朱嘉钢. 接口自动机的良构性检测算法及其实现[J]. 计算机应用, 2017, 7(2): 574-580.DOI: 10.11772/j.issn.1001-9081.2017.02.0574.
LI Xue, ZHU Jiagang. Well-formedness checking algorithm of interface automaton and its realization[J]. JOURNAL OF COMPUTER APPLICATIONS, 2017, 7(2): 574-580. DOI: 10.11772/j.issn.1001-9081.2017.02.0574.

基金项目

江苏省产学研项目(BY2013015-40)

通信作者

李雪(1990-),女,河南南阳人,硕士研究生,主要研究方向:软件工程、形式化方法,jndx_axue@163.com

作者简介

朱嘉钢(1957-),男,上海人,副教授,博士,主要研究方向:人工智能、模式识别、软件工程

文章历史

收稿日期:2016-07-22
修回日期:2016-08-28
接口自动机的良构性检测算法及其实现
李雪, 朱嘉钢    
江南大学 物联网工程学院, 江苏 无锡 214122
摘要: 针对构件式系统中任一构件的非良构性会导致系统不能正常运行的问题,提出一种基于接口自动机(IA)来分析和检测构件良构性(well-formedness)的算法,并据此实现了一个构件良构性检测原型系统。该算法首先构造与接口自动机同构的可达图;其次,基于可达图通过深度优先遍历生成一条覆盖所有迁移的有序集;最后,根据该有序集检测在外界环境满足其输入假设的情况下,每个属于方法的活动到其对应返回活动的路径的自治无异常可达性,从而实现接口自动机的良构性检测。根据所提算法在Eclipse平台设计并实现了构件良构性检测原型系统T-CWFC,该系统通过JFLAP建立构件的接口自动机模型并构造其可达图,进而对接口自动机作良构性检测并输出相关检测信息。最后通过对一组构件的良构性检测实验验证了算法的有效性。
关键词: 接口自动机    构件    良构性    最简运行    
Well-formedness checking algorithm of interface automaton and its realization
LI Xue, ZHU Jiagang     
College of IoT Engineering, Jiangnan University, Wuxi Jiangsu 214122, China
Abstract: To address the issue that the non-well-formed components in a component-based system may lead to the whole system working abnormally, an algorithm for checking the well-formedness of a component was proposed based on its Interface Automaton (IA) model, and a relevant prototype tool was developed. Firstly, the reachability graph isomorphic with the given IA was constructed. Secondly, an ordered set including all the transitions of the reachability graph relevant to the IA was obtained by depth-first-searching the reachability graph. Finally, the well-formedness check of a given IA was completed by checking whether each action belonging to a method in the IA could autonomously reach its return action without exception according to the ordered set under the condition that the external environment meets the input hypothesis. As a realization of the proposed algorithm, a relevant prototype tool was developed on Eclipse platform, namely T-CWFC (Tool for Component Well-Formedness Checking). The prototype tool can model the given component, set up its reachability graph, check its well-formedness and output check result message. The validity of the proposed algorithm was verified by running the tool on a set of components.
Key words: Interface Automaton (IA)    component    well-formedness    the most simple run    
0 引言

在软件开发过程中,基于构件的设计已成为处理复杂系统、提高生产力和产品质量的一个重要途径。构件封装特定功能,并通过接口(interface)来与构件式系统中的其他构件实现通信。在构建构件式系统时,对参与组合的构件的功能性和非功能性进行分析检测,是提高系统可靠性的有效途径之一。在检测已发现构件、重构的构件的良构性时,若发现其为非良构的,则必须拒绝其参与系统的构造[1]。为此,在组合构件系统、替换或细化现有构件式系统中的某个构件时,为使替换后系统正常运行,判断构件的良构性是必要的。

在构件良构性相关研究方面,诸多学者都作了有益的工作。文献[2]给出了良构性定义,认为接口是良构的,只要存在一种可以按照某种方式来适当选择其为接口所提供的输入来避免系统到达所有非法状态的环境时,即构件接口在其某个内部状态上不能接受某个输入时,外界环境不为其提供该输入[2]。该思想认为接口自动机(Interface Automaton,IA)是否是良构的,取决于是否存在一个合适的环境能够满足构件接口的所有输入假设而使非法状态不会达到,而未考虑在外界环境满足其输入假设时,接口自身内部的良构性。 文献[3]采用着色Petri网对Web服务进行建模,并在工作流网“良构性”定义基础上给出Web服务良构性定义,并指出服务的良构性能够保证组合服务可达终止状态的正确性。 文献[4]基于Petri网给出了服务流程是良构的当且仅当其具有活性和有界性 。文献[5]通过为接口自动机中每个状态添加时钟变量实现对具有实时特性的构件进行建模,并在文献[6]中提出的良构性基础上增加了时间良构性约束条件。 文献[7]则通过扩大接口自动机中自治活动的范围,在考虑外界环境满足构件需求的情况下,给出了接口自动机良构性的定义,即其与环境交互时接口内部自身能够正确运行而不会一直停留在某一状态,并指出当参与组合的接口自动机是良构的且其语义兼容时,则其组合系统也是良构的。但是,这些研究均未给出构件良构性的具体检测算法,只能由开发者自行根据定义描述来判定,降低了开发效率。

为此,本文首先提出了检测接口自动机良构性的算法。该算法利用接口自动机的可达图[8],通过深度优先遍历算法遍历可达图获取一条覆盖所有迁移的简单有序集,然后依次寻找有序集中每个方法活动到其对应返回活动间的最简运行并检测其自治无异常可达性,从而实现接口自动机良构性检测。当接口自动机中每个方法活动到其对应返回活动都是自治无异常可达的,则可得出该接口自动机是良构的。基于所提出的良构性检测算法,在Eclipse平台中实现了一个构件良构性的检测工具(Tool for Component Well-Formedness Checking,T-CWFC)。该检测工具的原型系统包括接口自动机建模模块、输入模型处理模块、构造可达图并获取简单有序集模块以及良构性检测和结果输出模块。最后,用上述原型系统对一组构件作良构性检测,得到了预期的结果,说明所提出的算法是有效的。

1 构件建模及其良构性

构件是一个包含提供接口和需求接口的软件单元[9]。构件的粒度可大可小,可以是一个类也可以是一个服务[10]。构件仅通过这些接口来与环境进行交互,因此常采用对接口进行形式化描述的方法来刻画构件的交互特性。本文采用接口自动机对构件进行建模,进而分析检测其良构性。

1.1 接口自动机及其良构性

传统的接口自动机理论将构件中的每个活动看作是一个输入、输出或内部活动。在刻画活动的语义信息时,文献[7]将每个活动进一步细化为方法活动、返回活动和异常活动等三种类型,并给出了接口自动机良构性定义。

为了描述方便,本文用符号“a?”“a!”和“a;”分别表示输入活动、输出活动和内部活动,其中a为活动名。类似地,用符号“m”“r”和“e”分别表示活动类型为方法类型、返回类型和异常类型。IA的形式化定义如下。

定义1 接口自动机(Interface Automata,IA)[7]。接口自动机P是六元组P=(VP,vPInitPIPOPH,δP)。其中:VP是状态的有穷集合;vPInitVP是初始状态集,且vPInit不为空;Σ PI、Σ PO和Σ PH分别为P的输入、输出和内部活动集合;δPVP×ΣP×VP 是迁移的集合。

文献[6]中将P的所有活动集合记为ΣP,即ΣPPI∪Σ PO∪Σ PH。 为了描述接口自动机的良构性,文献[7]将P中的输入活动Σ PI进一步细分为输入方法活动Σ PIm、输入返回活动Σ PIr和输入异常活动Σ PIe,显然有Σ PIPlm∪Σ PIr∪Σ PIe。同理,Σ POPOm∪Σ POr∪Σ POe和Σ PHPHm∪Σ PHr∪Σ PHe。则P中所有方法活动可记为Σ PmPIm∪Σ POm∪Σ PHm,所有活动集合记为ΣPPm∪Σ Pr∪Σ Pe

文献[7]中,对于P中任意方法活动a∈Σ Pm,其签名为a(i1:$\mathbb{Z}$[i1],i2:$\mathbb{Z}$[i2],…,ik:$\mathbb{Z}$[ik])→o:$\mathbb{Z}$[o]#e。其中,v:$$\mathbb{Z}$[v]是v的类型,{i1,i2,…,ik}是活动a的输入参数集合。同样,本文记Rp(a)=o是方法活动a的返回活动,Ep(a)=eP中方法活动a的异常活动。另外,对于外界环境提供的活动信息,接口自动机可以根据需要自行控制是否接受的活动为自治活动[3]。为此,文献[7]中提出接口自动机中除了异常活动和输入方法活动外,其余都是自治活动。有关接口自动机中的自治活动和无异常活动描述如下。

对于接口自动机P,其自治活动集合为Σ PautP\(Σ Plm∪Σ PIe)。对于P中活动a,当其不属于异常活动(即a∉Σ Pe)时,则称a是无异常活动,记无异常活动集合为Σ PnoExcPPe。由此可知,对于P中的活动a,当其满足a∈Σ Pauta∈Σ PnoExc时,则称活动a为自治无异常活动,记P中自治无异常活动集合为Σ Paut_noExcP\(Σ Plm∪Σ Pe)。

对于接口自动机P中的集合Σ P*中,从状态vVP使能的活动集合为Σ P*(v),其中*∈{I,O,H,Im,Om,Hm,Ir,Or,Hr,Ie,Oe,He,m,r,e,aut}。由此可知,P中从状态vi使能的方法活动为Σ Pm(vi);从状态vi使能的返回活动和异常活动分别为Σ Pr(vi)和Σ Pe(vi)。

定义2 运行和可达的(run and reachable)[6]。接口自动机P中的运行是状态和动作的有限交替序列v0,a0,v1,a1,…,vn且对于所有的i(0≤in)时(vi,ai,vi+1)∈δP。考虑两个状态v,uVP,若在vu之间存在一个起始状态为v、终止状态为u的运行,则称u是从v可达的。

定义3 良构性(well-formed)[7]。接口自动机P是良构的,当且仅当对于P中所有状态vVP,且活动a∈Σ Pm(v),其返回活动RP(a)∈Σ Pr时,则P中至少存在一个状态uVP,其中RP(a)∈Σ Pr(u),是可从Succp(v,a)自治且无异常可达的。

定义3中的符号Succp(v,a)代表状态v接收到活动a后能够到达的状态。定义3认为构件在与环境交互过程中,只要其能够接收各个方法活动的返回活动时,接口自动机中存在一条可控且能够无异常到达使能其返回活动的状态的运行即认为接口自动机是良构的。

1.2 最简运行和自治无异常可达

在构件式系统中,对于任一构件,系统中的其他构件可看作是其工作环境。接口自动机描述了构件接口的时序特性,同时将接口的输出保证和输入假设整合在一起,其中输出保证相当于接口对环境所作的假设;输入假设则相当于接口自身行为的一种描述[2]。外界环境总是能够满足其要求,即当P需要接收(或发送)消息时,外界环境总是能够适时地发送(或接收)该消息,从而能够排除因外界环境导致接口自动机中运行出现死锁的情况[3]

由定义3可知,在外界环境满足其输入假设时,检测构件的良构性需要:1) 首先找到Succp(v,a)到使能其返回活动Rp(a)的状态uVP之间的运行;2) 判断该运行中包含的活动是否是自治无异常的。然而,当接口自动机P中存在环路或存在多次调用方法活动a时,状态v和使能Rp(a)的状态u之间的运行路径将随着环路执行的次数不同而可能使两状态间的运行数目和运行所经过的状态数是无穷的、不确定的。在此,为了检测构件的良构性,本文考虑两状态间的最简运行来保证运行中不会出现循环执行某一个环路的情况,从而使状态vu的运行数目具有确定性,运行长度具有最短性。

定义4 最简运行(the simple run)。对于接口自动机P中状态vivj间的运行η=viaivi+1…vj-1aj-1vj且(ij),若η进一步满足下列条件,则称运行η是最简运行:1) 对于任何正整数m,k且imjη中均不存在任何运行vmamvm+1…am+k-1vm+k-1vm+k使得vm=vm+k;2) 若存在另一条从vivj的运行η′,必有η′所含有的状态数不小于η中所含有的状态数。

定义4是在定义2的基础上,对运行中的环路和运行长度添加了限制条件。特别地,用集合Ση表示最简运行η中所有被使能的活动ai,ai+1,…,aj-1

另外,文献[7]根据对活动的不同分类将两状态间的运行分为自治运行(autonomous run)和非自治运行(non-autonomous run)。由此两状态间的可达性可分为自治可达(reachable autonomously)和非自治可达(reachable non-autonomously)。为了方便下文中形式化描述构件良构性检测,结合定义2和4给出了最简自治无异常可达定义。

定义5 最简自治无异常可达(the simple reachable autonomously without exceptions)。对于P中的任意两个状态vivj,若存在运行η,且其初始状态为vi,终止状态为vj。当η同时满足下列条件时,称vjP中从vi自治无异常可达,记为viηaut_noExc vj${{v}_{i}}{{\xrightarrow{\eta }}_{aut\_noExc}}{{v}_{j}}$:1) 运行η是最简运行η′;2) 集合Ση中每个活动a均为自治活动,即a∈Σ Paut;3) 集合Ση中每个活动a均为无异常活动,即活动a∈Σ PnoExc

定义5的条件1) 对状态vivj之间的运行η中的回路 和路径长度进行限制,条件2) 和3) 则是对最简运行中涉及到的活动的具体类型进行判断。特别地: (a)当运行η的初始状态vivPInit,则称vjP中是可达的;否则,称vjP中是不可达的。 (b)当运行η仅满足条件1) 和条件2) ,则称vjP中可从vi最简自治可达,记为${{v}_{i}}{{\xrightarrow{\eta }}_{aut}}{{v}_{j}}$。 (c)当运行η仅满足条件1) 和3) ,则称vjP中可从vi是最简无异常可达的,记为${{v}_{i}}{{\xrightarrow{\eta }}_{noExc}}{{v}_{j}}$

文献[7]中将每个方法活动的返回值细分为返回活动和异常活动两种。由此,文献[6]所给出的通信构件User的输出保证,即对外界所作的假设为环境提供了方法活动msg,并在User调用方法活动msg时,给出相应的通信成功ok和通信失败fail信息。而构件User并未对通信失败活动fail有任何响应,则认为User的外部环境不能满足其输入假设。此时构件User在与其环境组合时依然会因非同步活动而引入非法状态。

针对此情况,本文结合文献[2]和[7]来检测构件的良构性,即本文在检测接口自动机P的良构性时,在外界环境总是能够满足P对外部消息需求的情况下,且对于P中所有状态vVP,当方法活动a∈Σ Pm(v)时,考虑如下几种情况:

1) 方法a的返回活动RP(a)或异常活动EP(a)不在P可接受范围,即RP(a)∉Σ Pr∪EP(a)∉Σ Pe

2) 方法活动a的返回活动和异常活动满足RP(a)∈Σ Pr∩EP(a)∈Σ Pe的同时P中至少存在一个状态uVP,其中RP(a)∈Σ Pr(u),且Succp(v,a)与状态u之间不存在一条最简运行使u是可达的;

3) 方法活动a的返回活动和异常活动满足RP(a)∈Σ Pr∩EP(a)∈Σ Pe的同时P中至少存在一个状态uVP,其中RP(a)∈Σ Pr(u),且Succp(v,a)与u间至少存在一条最简运行使u是可达的,但不是自治无异常可达。

以上的条件1) 描述了构件中方法活动的返回活动或异常活动不在构件可接受范围之内的情形,即外界环境不满足构件的输入假设。条件2) 和3) 描述了构件在输入假设满足的情况下,不能满足方法活动到使能其返回活动的状态是可控且能够到达的情形,即构件会一直停留在某一状态而使构件失效。

接口自动机的组合参考文献[6]定义10所描述的接口自动机组合方法,关于良构的接口自动机及其组合的一个重要结论如下:设两个接口自动机分别为P1P2P1P2能够组合且其组合为P=P1P2,若接口自动机P1P2是良构的,则其组合P是良构的。

2 良构性检测算法实现

通过1.2节对构件良构性检测的几种情况的分析可知,在外界环境满足其输入假设时,为检测构件的良构性,首先需要获取从方法活动到使能其返回活动的状态间的运行;其次,判断该运行是否是自治无异常的。下面将分别给出具体实现算法。

2.1 获取两状态间运行方法

文献[8]中在验证构件式系统与需求规约的一致性时,为获取构件式系统的任一行为,给出了构造与构件式系统同构的可达图的方法,并证明了构件式系统的任一行为都会对应可达图中的一条路径。然而,当可达图中存在环路,此时路径的数目可能是无穷的,路径的长度也可能是无穷的[8]。为此,本文首先构造与IA同构[11]的可达图,其次通过深度优先遍历(Depth-First Search,DFS)来实现自动生成一条覆盖自动机中所有迁移且不包含重复迁移的有序集,最后根据有序集获取任意两状态间的运行。可达图的构造方法见文献[8]。

在采用DFS方法遍历图的过程中,碰到环路且判定当前节点已访问过时,便回溯,此时环路中的部分转换边则会在有穷的遍历中被漏掉。为解决上述问题,本文引入简单有序集的概念,并给出通过DFS遍历G得到简单有序集的实现算法,见算法1。

对于可达图G=(V,T),且其有穷边集T的个数为NumT,通过DFS遍历得到的任一条有序集P=t0t1…tn是简单有序集,若有序集P同时满足:1) 对于任何i,j(0≤ij≤n),ti≠tj;2) 有序集P中转换边个数n=NumT

算法1  DFS遍历边序列生成算法。

输入  可达图G=(V,T),V≠∅,T≠∅。

输出  R={〈vi,af,vjk|k满足对G的DFS顺序}。

1)  初始化:G′=(V′,T′)⇐G,R⇐∅,k⇐1;

2)  v1tv0V′; //取出第一个顶点

3)  若存在viV′且〈v1t,ak,vi〉∈T′,则

  v2t⇐v′i;R=R+{〈v1t,ak,v2t〉};kk+1;T′=T′-{〈v1t,ak,v2t〉};v1tv2t;

  循环以上操作直到T′=∅,转5) ;

4)  取任意viV′且〈v′i,ak,v1t〉∈R;

  v1tvi,转3) ;

5)  结束。

2.2 构件良构性检测算法

通过2.1节引入的简单有序集概念,将采用DFS遍历可达图时可能得到的有序集的个数和有序集长度均限制在有穷有序集中。此时,根据该有序集检测构件良构性则需要循环依次检测有序集中每个方法活动到使能其返回活动的状态是否是可达的且是自治无异常可达的。根据1.2节可知,在检测构件的良构性时,需获取该两状态间的最简运行。而根据算法1得到的有序集有可能包含环路的和不连续的,为此首先需要将两状态间的有序集化简为最简运行,然后根据最简运行来检测从方法活动是否能够自治无异常地到达使能其返回活动的状态。为此,本文给出将两状态间的简单有序集化简为最简运行的方法。

设遍历G得到的有序集path中任意两个节点vivj间存在一个有序集η=(vi,ai,vi+1) (vm,am,vm+1)… (vj-1,aj-1,vj),且η不是最简运行,则执行以下步骤将其化简成最简运行:

1) 对η中任意相邻转换边(vp,ap,vp+1)(vq,aq,vq+1),若vp+1≠vq,则取path中起始节点为vp+1,终止节点为vq之间的有序集添加至η中的该相邻转换边之间,得到有序集η′;

2) 路径η′中,对于任意m,n(imnj-1) ,若存在(vm,am,vm+1)…(vn,an,vn+1)使得vm=vn,则删除η′中转换边(vk,ak,vk+1)(mkn);

3) 重复1) 和2) ,直到有序集η是最简运行。

基于以上分析,根据已得到的可达图有序集检测构件良构性的算法详见算法2。算法2的输入为有序集、方法和其对应返回动作的关系集合Σ Pflag以及自治无异常活动集合Σ Paut_noExc。其中,有序集可通过算法1遍历可达图得到;Σ Pflag则易根据接口自动机和文档说明得到,元组〈mi,ri,ei〉中mi为方法活动,riei为方法mi对应的返回活动和异常活动,且当其返回或异常活动为空时,其值为null;而Σ Paut_noExc则可从Σ Pflag中根据1.1节介绍的自治无异常概念得到。

算法2 构件良构性检测算法。

输入 R={〈vi,af,vjk|k满足对G的DFS顺序},Σ Pflag={〈mi,ri,ei〉},Σ Paut_noExc={aq|aq为自治无异常活动}。

输出 构件是否为良构的布尔值isWell;构件为非良构时的错误记录rst

1)  初始化:k⇐1,flag⇐true,isWell⇐false,rst⇐∅;at⇐null,

  ae⇐null,run⇐∅,N⇐|R|;M⇐|run|;

2)  检测每个mi到对应ri的自治无异常可达性:

a)  取af满足〈vi,af,vjkR;

b)  若存在i满足af=mi且〈mi,ri,ei〉∈Σ Pflag,则

c)   atriaeei;

d)   若〈vi,at,vj〉∈R且〈vi,ae,vj〉∈R,则

e)    若tkrun⇐{〈vi,af,vjx|kxt};

f)    否则run⇐{〈vi,af,vjx-k+1|kxN}∪{〈vi,af,vjx+N-k+2|0≤xt};

g)    否则flag⇐false;rstrst∪{at,ae},转o);

h)   对run进行去环操作,使run满足:对于任意〈vi,ax,vj〉∈R,均不存在另一个〈vi,ax,vj〉∈R,使得vi=vi

i)   对run进行连接操作,使run满足:对于任意〈vi,ax,vj〉∈R′,若存在右侧相邻〈vi,ax,vj〉∈R′,有vj=vi;

j)   重复执行一次步骤h)、i);

k)   取ax满足〈vi,ax,vj〉∈run;

l)   若ax∉Σ Paut_noExc,则 flag⇐false,

   rstrst+{ax∉Σ Paut_noExc};

m)   xx+1;

n)   若xM,则转k);

o)   kk+1;

p)   若kN,则转2) ;

3)  若flag=true则isWell⇐true;

   否则isWell⇐false;

4)  结束。

算法2中的步骤2) 则是依次取出有序集R′中的每个元组〈vi,ak,vj〉,并在环境满足构件的输入假设时,判断R′中方法活动mi到其对应返回活动ri之间的自治无异常可达性。其中,步骤c)~f)则为方法活动对应的返回活动满足构件的输入假设时,在有序集R′中取出方法操作与其返回活动间的有序集run;步骤h)~j)则是根据2.2节介绍的最简运行化简方法,将已获取的有序集run化简为最简运行;步骤k)~n)则是循环检测最简运行run中每个元组所包含的活动是否是自治无异常活动,若其中任意一个活动不是自治操作则布尔值flag为false,从而实现在算法结束时根据flag值来判定构件的良构性。

在该良构性检测过程中,在外界环境满足构件的输入假设时,只要两节点间的最简运行不符合良构性定义3则该接口自动机即为非良构的。因文中引入了最简运行概念,所以遍历与IA模型同构的可达图时,得到的简单有序集长度是有限的,则算法2是可终止的,且其算法复杂度随G中节点数和方法活动个数的增加而增加。

3 良构性检测系统实现及实例应用

基于以上理论分析,本文设计了一个构件良构性检测原型工具T-CWFC。该原型工具采用具有良好的跨平台运行特征以及丰富的类库资源的java作为工具的实现语言,并使用Eclipse的插件技术来设计和开发T-CWFC,因此,该工具易于在 Eclipse环境中通过插件技术来安装、配置和使用。T-CWFC的目的是应用于构件式软件开发的设计建模阶段,对构件的良构性进行形式化的分析和检测,从而保证组合系统能够正常运行,为系统的其他功能性分析和验证等作准备。

3.1 良构性检测系统实现

构件良构性检测工具T-CWFC中模型分析和检测基本流程如图 1所示(其中,黑色圆点节点为开始,矩形节点为系统的输入和输出):首先对IA模型进行输入处理;其次基于DFS算法分析得到覆盖被测构件的IA模型中所有迁移的有序集;然后根据构件外界环境需求和有序集实现良构性检测,最后给出检测结果和相应错误报告。

图 1 T-CWFC的模型良构性检测流程的活动图 Figure 1 Activity diagram of well-formedness checking in T-CWFC
3.1.1 IA模型输入处理

接口自动机是有限自动机的扩展,是一种特殊的自动机[6]。JFLAP(Java Formal Languages and Automata Package)[12]是一款Java语言编写的开源工具,它不仅提供了方便易用的有限自动机建模接口,而且提供了在有限自动机中添加一些文本和标签的功能。为此,本文采用JFLAP工具建模接口自动机模型并为接口自动机的每个操作添加相应的类型标签,然后将保存得到的.jff文件作为T-CWFC的输入。T-CWFC系统中,为获取构件的简单有序集,首先需对输入进行解析,即对输入.jff文件进行解析处理得到接口自动机的状态、迁移、活动名和活动类型等信息。以下给出文献[6]中通信构件User的接口自动机模型对应的.jff文件示例说明。其中:标签<type>标明该接口自动机为有限接口自动机;标签<text>则是建模时添加的标签信息,即描述了系统环境和构件内部的方法活动和其相应返回活动、异常活动。

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
  <structure>
   <type>fa</type>   <!--有限接口自动机--->
   <automaton>   <!--自动机--->
    <!--The list of states.-->
    <state id="0" name="s0"> <!--状态名和ID--->
     <x>176.0</x>
     <y>117.0</y>
     <initial/>   <!--初始状态--->
    </state>
    <state id="1" name="s1">
     <x>299.0</x>
     <y>119.0</y>
    </state>
    <!--The list of transitions.-->
    <transition>   <!--迁移--->
     <from>1</from>  <!--迁移的起始状态ID--->
     <to>0</to>  <!--迁移的终止始状态ID--->
     <read>ok?</read> <!--迁移中的动作名和类型--->
    </transition>
    <transition>
     <from>0</from>
     <to>1</to>
     <read>msg!</read>
    </transition>
    <note>   <!--输入、输出操作--->
     <text>output method:msg,<!--输出方法操作--->
     input return:ok,  <!--输入返回操作--->
     input exception:fail;</text> <!--输入异常返回操作--->
     <x>136.0</x>
     <y>50.0</y>
    </note>
   </automaton>
  </structure>

通过使用Java类库中文档对象模型(Document Object Model,DOM)方法可以很方便地对IA模型进行解析,并根据Automata、Transition、Action以及 State等实体类定义在内存空间生成并创建相应的自动机对象;同时,得到存储每个方法活动与其相应返回活动、异常活动的集合Σ Pflag

3.1.2 获取简单有序集

3.1.1节已通过解.jff文件在内存中创建了IA模型对象。为获取包含IA模型的所有迁移且不具有重复迁移的有序集,本文采用文献[8]中构建与接口自动机网络同构的可达图方法,逐个读取已创建的数据结构State中的状态信息来构建可达图的顶点,并利用已创建的Transition和Action来创建可达图中的各条边,从而在内存中构造一个与接口自动机对象相对应的可达图,进而采用DFS遍历该可达图得到一个简单有序集。获取可达图中简单有序集的流程如图 2所示。

图 2 简单有序集获取的流程 Figure 2 Flow chart of extracting the simple ordered set

遍历可达图生成简单有序集的算法见算法1。算法的输出是一条简单有序集,该简单有序集形如(s0,m1,s1) →(s1,m2,s2) →…→(sp,mn,sq),且mx(1≤x≤n)是IA中的动作,sx(1≤x≤q)是IA中的状态。另外,在T-CWFC生成的有序集中,对每个迁移中包含的动作mx的类型也进行了详细的标注,即明确标注其为方法“m”(或返回“r”或异常“e”)活动和输入“?”(或输出“!”或内部“;”)类型。

3.1.3 良构性检测

由3.1.2节的分析可知,DFS遍历可达图时得到的有序集的个数和有序集长度均为有穷的。根据时序特性可知,无论IA中的内部状态转移是顺序、选择还是并行结构,接口自动机中每个方法活动执行之后,才会接收或发送其返回活动和异常活动,因此在接口自动机中不存在先使能返回或异常活动再使能其方法活动的情况出现。由此,根据3.1.1和3.1.2节得到的系统输入和简单有序集即可利用2.2节给出的算法2对构件的良构性进行检测。

图 3给出了构件良构性检测工具T-CWFC工具中IA模型良构性检测的类图框架。该类图框架主要包括自动机模型核心类、构造与IA同构可达图的Graph、Vertex和createGraph类、检测良构性相关类(其包括wellFormedDetect class和dfsTraversal类)以及表示外界环境信息的Message类和解析jff文件的辅助工具类parJffTools class和parseInfo class。

图 3 T-CWFC中良构性检测类图 Figure 3 Class diagram for well-formedness checking in T-CWFC

在良构性检测类(wellFormedDetect class)的实现过程中,其中一个关键的问题为:在判定IA模型的良构性时,需要首先获取方法活动到其返回活动间的最简运行,然后根据定义5来进行判定。而直接从dfsTraversal类得到的简单有序集中获取的两状态间的路径有可能不是最简运行。为此,在实现类wellFormedDetect时,本文系统首先根据2.2节给出的化简方法将两状态间的路径化简为最简运行,然后按照算法2实现良构性检测,并给出良构性检测的过程和结果报告。在实际中亦会出现构件中的同一方法活动发生两次且其返回活动亦可能出现两次的情况,则需要准确确定该方法活动与其相应返回活动的运行,本系统在实现过程中对这种情况也作了相应处理,从而保证构件良构性检测的正确性。

3.2 应用实例

本文设计和实现的T-CWFC模型检测工具是在Windows 7活动系统平台,eclipse 4.3.2 、 java jdk 1.7和JFLAP 7.0环境下开发。本节以文献[6]中所给出的通信构件Comp和User的接口自动机模型对T-CWFC模型检测工具进行应用说明。

在JFLAP中建立的具有类型信息的构件Comp和User模型如图 4所示。其中,图 4(a)的IA模型描述了构件Comp在假设环境确定下与环境交互的行为特征:即其假设环境提供了send方法活动,且在该方法活动被调用时给出相应的返回活动ack和异常活动nack,所以当Comp中方法活动msg被外部调用时,构件将先调用send方法活动与其环境进行交互,并在接收环境提供的返回活动ack之后,向调用者返回通信成功信息ok;若连续两次send请求活动接收到的都是一次活动nack,则向通信者返回通信异常fail。图 4(b)的IA模型描述了构件Comp的使用者构件User在假设环境确定下的行为特征,其对环境的假设为当其调用环境Comp提供的msg消息时,则会得到通信成功ok信息和通信异常fail信息。

图 4 通信构件的IA模型 Figure 4 IA models of communication components

根据良构性定义5就能从直观上判断Comp是良构的,而User对外界环境提供的通信异常活动无响应,在外界环境满足其输入假设时则是良构的。运行T-CWFC进行User和Comp良构性检测的结果如图 5所示。其中:界面左边的“JFLAP建模IA”按钮则是利用有限自动机建模JFLAP插件用于对接口自动机进行建模;“选择(IA)jff文件”则是选择待检测构件的建模文件;“良构性检测”按钮则是根据算法1和2检测所选的jff文件的良构性,并在界面的右侧文本区域显示出检测结果。

图 5 通信构件的T-CWFC运行界面 Figure 5 GUI of communication components in T-CWFC

图 5(a)中所给结果显示构件User未对通信异常活动作出响应,具体检测结果信息为:通过DFS遍历其相应可达图得到的简单有序集为(s0,msg!m,s1) →(s1,ok?r,s0) ,且对于方法活动msg达到的状态s1到使能返回活动ok的状态之间是自治无异常可到的。而对于构件User在初始状态s0调用外部环境提供的方法活动msg后迁移到s1后,并未对外部环境提供的通信异常消息fail作出相应的响应,即当构件Comp的输出信息fail是构件User的输入时,构件User将一直停留在状态s1。由此可见,运行T-CWFC检测的结果与根据定义5得到的相同,即异常返回是不正确的结论。此时,在构件User与其他构件参与组合时,即可根据检测得到的结果指导设计者提供合适的外界环境来满足其输入假设从而保证该构件是良构的。

图 4(b)显示Comp的IA模型中存在三个环路,且从状态s2和s4到初始状态s0均分别有两个选择分支,则对Comp对应的可达图进行DFS遍历时共有四条简单有序集。图 5(b)显示运行T-CWFC得到的简单有序集(s0,msg?m,s1) →(s1,send!m,s2) →(s2,nack?e,s3) →(s3,send!m,s4) →(s4,nack?e,s6) →(s6,fail!e,s0) →(s4,ack?r,s5) →(s5,ok!r,s0) →(s2,ack?r,s5) 是DFS遍历可得到的。对于构件Comp中提供的方法活动msg,从图 4(b)可分析出使能其返回活动ok的状态为s5,且从s1到s5的最短路径为(s1,send!m,s2) →(s2,ack?r,s5) 。图 5(b)的结果显示,方法活动msg到使能返回活动ok之间的简单有序集为(s1,send!m,s2) →(s2,nack?e,s3) →(s3,send!m,s4) →(s4,nack?e,s6) →(s6,fail!e,s0) →(s4,ack?r,s5) →(s5,ok!r,s0) →(s2,ack?r,s5) ,该有序集所包含的迁移中存在具有相同起始状态的迁移,且其中的部分相邻的两个迁移中存在前一个迁移的终止状态不等于后一个迁移的起始状态的情况,即DFS遍历得到的有序集中存在环路和不连续迁移,按2.2节的最简路径化简方法去除环路并将不连续的路径变成连续得到的最简运行为(s1,send!m,s2) →(s2,ack?r,s5) ,根据定义4可知,从s1到s5是自治无异常可达的。

同理,图 5(b)的运行结果显示:首次调用方法活动send的终止状态s2到使能其返回活动的s2的运行和化简后的运行、第二次调用方法活动send的终止状态s4到使能其返回活动的s4均与实际分析得到的相同,且发现该两种方法活动到达的状态与使能其返回活动的状态相同,即自治无异常可达的。

利用本文提出的算法2对构件Comp和User的良构性检测已结束,且其检测结果与分析结果是一致的。由此可见,本文提出的基于接口自动机的构件良构性判定算法是有效的。

4 结语

本文基于接口自动机理论给出了一种检测构件良构性的算法,并根据该算法在Eclipse平台设计并实现了检测构件良构性的原型工具T-CWFC。该工具可应用于构件式系统软件开发的设计建模阶段,对参与组合系统的构件的自身良构性进行分析和检测,有助于设计者尽早发现错误并采取相应措施予以修正处理,从而实现一次性正确构造系统来降低成本并提供系统可靠性。本文只给出了检测参与组合构件的良构性检测算法,后续工作中则将对该原型工具T-CWFC继续完善,以加入构件式系统的其他功能性测试等。

参考文献
[1] STEIMANN F. From well-formedness to meaning preservation:model refactoring for almost free[J]. Software & Systems Modeling, 2015, 14 (1) : 307-320.
[2] 张岩, 胡军, 于笑丰, 等. 接口自动机——一种用于组件组合的形式系统[J]. 计算机科学, 2005, 32 (11) : 212-217. ( ZHANG Y, HU J, YU X F, et al. Interface automata-a formal system for components composition[J]. Computer Science, 2005, 32 (11) : 212-217. )
[3] 李喜彤, 范玉顺. Web服务流程相容性和相似性分析[J]. 计算机学报, 2009, 32 (12) : 2429-2437. ( LI X T, FAN Y S. Analyzing compatibility and similarity of Web service processes[J]. Chinese Journal of Computers, 2009, 32 (12) : 2429-2437. )
[4] REISIG W. Well-formed system nets[M]. Berlin: Springer-Verlag, 2013 : 169 -172.
[5] DE ALFARO L, HENZINGER T A, STOELINGA M, et al. Timed interfaces[C]//EMSOFT 2002:Proceedings of the 2nd International Conference on Embedded Software, LNCS 2491. Berlin:Springer-Verlag, 2002:108-122.
[6] DE ALFARO L, HENZINGER T A. Interface automata[J]. ACM SIGSOFT Software Engineering Notes, 2001, 26 (5) : 109-120. doi: 10.1145/503271
[7] MOUELHI S, AGROU K, CHOUALI S, et al. Object-oriented component-based design using behavioral contracts:application to railway systems[C]//CBSE'15:Proceedings of the 18th International ACM Sigsoft Symposium on Component-Based Software Engineering. New York:ACM, 2015:49-58.
[8] HU J, YU X, WANG L, et al. Scenario-based specifications verification for component-based embedded software designs[C]//ICPPW'05:Proceedings of the 2005 International Conference on Parallel Processing Workshops. Washington, DC:IEEE Computer Society, 2005:240-247.
[9] SHAI O, PREISS K. Isomorphic representations and well-formedness of engineering systems[J]. Engineering with Computers, 1999, 15 (4) : 303-314. doi: 10.1007/s003660050025
[10] 雷斌, 王林章, 卜磊, 等. 基于状态机模型的构件健壮性测试[J]. 软件学报, 2010, 21 (5) : 930-941. ( LEI B, WANG L Z, BU L, et al. Robustness testing for components based on state machine model[J]. Journal of Software, 2010, 21 (5) : 930-941. doi: 10.3724/SP.J.1001.2010.03544 )
[11] 王文霞. 有向图的同构判定算法:出入度序列法[J]. 山西大同大学学报(自然科学版), 2014, 30 (2) : 10-13. ( WANG W X. An isomorphism testing algorithm for directed graphs:the in-degree and out-degree sequence method[J]. Journal of Shanxi Datong University (Natural Science Edition), 2014, 30 (2) : 10-13. )
[12] RODGER S H, FINLEY T W. Jflap:An Interactive Formal Languages and Automata Package[M]. Sudbury: Jones & Bartlett Publishers, 2006 : 1 -15.