基于命题逻辑的组件约束检测

基于命题逻辑的组件约束检测摘要:针对组件约束数量大、复杂度高的问题,提出了一种基于命题逻的组件约束检测算法.通过命题符号化的过程,即通过个联结词将日常语言中的命题转化成数理逻中的形式命题.该算法首次使用受限真值表的概念来描述组件约束,清楚、准确地揭示了软件组织结构、动态行为以及组件之间的转换,通过包含、否定和插入等规则来合并真值表,以解决检测组件约束时存在的冗余与冲突问题,并获得期望行为的最小组件集合,从而保证了组件约束之间相互一致.与基于规则模式表方法相比,所提算法克服了人工检测的不确定性,改善了检测的时间性能,并可将冲突错判率降低大约10%,平均处理时间降低大约33%.关键词:组件约束;命题逻;真值表;检测算法ComponentConstraintDetectionBasedonPropositionLogicChenNing,FengBoqinAbstract:Aimingattheproblemthatthereexistsverycomplicatedandalargeamountofcomponentconstraints,analgorithmofcomponentconstraintdetectionbasedonpropositionlogicwasproposed,inwhichthepropositionindailydictionwastransformedintotheformalpropositionofmathematicallogicviatheprocessofpropositionsymbolization,i.e.fiveconnectivewords.Theproposedmethodutilizestheconceptofconstrainedtruthtabletodescribethecomponentconstraints,andthesoftwarearchitecture,dynamicbehaviorandtransformationamongcomponentsarerevealedtransparentlyandexactly.Thetruthtableisincorporatedbyinclusion,negationandinsertionrulestosolvetheproblemofredundancyandconflictexistingindetectingthecomponentconstraints.Moreover,aminimalsetofrulesoftheexpectedbehaviorisobtainedtoensuretheconsistencyofcomponentconstraints.Comparedtotheexistingrulepatterntableapproach,theuncertaintyinmanualdetectionisovercomeandthetemporalperformanceofdetectionisimproved.Themisjudgmentofconflictisdecreasedby10%andtheaverageprocessingtimeisloweredbyabout33%.Keywords:componentconstraint;propositionlogic;truthtable;detectionalgorithm在基于组件的软件开发过程中,组件之间的复杂关系形成了组件约束.不同的组件分析人员在发现、描述以及修改组件约束时会引入冗余与冲突等异常问题,这些问题将增加软件系统开发和维护的成本,甚至使得软件系统产生不期望的行为。少量的简单约束的手工检测易于实现,但随着约束数量以及复杂度的增加,它已显得无能为力.本文提出了基于命题逻辑的自动检测算法,以检验组件约束的冗余与冲突.其中,用冗余检测来保证约束的独特性,实现经济约束集,即软件可以得到期望行为的最小集合的组件,而用冲突检测来保证组件约束在使用时的一致性..1命题演算定义1符号化的命题称为命题公式,其形式化定义如下.(1)命题变元以及T、F是命题公式(2)如果a是命题公式,则a也是命题公式.(3)如果a、b是命题公式,则(ab)、(ab)、(a→b)、(ab)都是命题公式.(4)有限次使用形式化定义(1)~定义(3)构成的符号串为命题公式.在定义1中,以真、假为变域的变元称为命题变元,如果一个命题公式中含有n个不同的命题变元,则称其为n元命题公式.定义2将真值表定义为n元命题公式a,对于所有不同指派下的真、假值排列,其中的指派是指在n元命题变元的真值确定后的取值序列。定义3将组件约束形式化定义为一个命题公式f则有lhs(f)→rhs(f),其中lhs(f)为公式f的左端,称为前提,表示为p1p2pn,pi为一个原软件系子命题,又称为条件命题,|lhs(f)|为所有条件命题的个数,任意pi与pj之间的操作符号为AND,表示为;rhs(f)=q为公式f的结论,其中q为一个原子命题,又称为结论命题.命题演算是一种形式语言,其目的在于将数个联结词将日常语言中的命题转化成数理逻辑中的形式命题.每个约束的任意条件命题以及结论命题都赋给一个真值.如果执行命题,真值为1(真),否则真值为0(假).任意组件约束f如果满足前提触发,则一定会触发结论的执行.也就是说,在组件约束中,条件命题都为1,而结果命题为0的情况没有意义.可见,组件约束并不要求所有真值是枚举的,因此可用受限的真值表表示组件约束前提与结论之间的逻辑关系.受限的真值表排斥组件约束中不可能情况的真值,例如构建的组件约束p1p2→q的真值表如表1所示,显然只有第1、第8行有实际意义,表示这条约束能否执行.在真值表中,每个真值指派都包括了所有的原子命题公式以及复合命题公式,而在组件约束的实际应用中,只需要前提与结论的原子命题的真值.因此,根据组件约束的应用需要,受限真值表只需包含条件命题与结论命题的真值指派为1的情况.定义4组件约束x的受限真值表的形式化表达式为(x)=(p1,…,pn,q),其中p1,,pn为条件命题,q为结论命题,而对应命题的真值指派(x)=(p01,p02,,pn0,q)其中p1，p2…,pn为条件命题。Q为结论命题。而对应命题的真值指派（x）=(p01,p02,…,pn0,q0),其中pi0=1,ni1,10q,指派个数|(x)|=1.2组件系统异常检测检测组件约束冗余和冲突的目标是帮助软件系统产生一个最小无冲突的组件约束集合.下面给出冗余和冲突的定义,并提出一系列检验步骤.定义5冗余是指一条组件约束存在多个版本.例如,组件约束pipj→q与pjpi→q除了条件命题顺序有所不同,表达的内容是一致的.定义6突是指不一致性,包括前提不一致性与结论不一致性,前者指组件约束的条件命题不一致,而结论命题一致,例如pipj→q与pipj→q;后者指组件约束的条件命题一致，而结论命题不一致,例如pipj→q与pipj→q.基于命题逻辑的检验方法的核心思想是:先为组件约束生成受限真值表,再利用一套规则来合并冗余与冲突的组件约束.最后通过定理来识别存在冗余与冲突的组件约束。21构建组件约束的有限真值表基于定义1,为每条组件约束生成受限真值表,其中组件约束的前提划分为多个条件命题,论划分为一个结论命题,而构建的受限真值表只包含真值都为1的一行.22合并真值表x,y为2条约束,(x)=(p1,…,pm,q),(y)=(p1,…,pn,q),其中p1,,pm为x约束的条件命题,q为结论命题,p'1,p'2,…,pn'和q'分别为y约束的条件、结论命题,合并的真值表为(xy)(初为空),则本文提出合并真值表的3条规则描述如下.(1)包含规则.如果pi→pi,可将pi添加到(xy)作为条件命题,且约束x、y在此命题列的真值取值分别为1.(2)否定规则.如果pipi’,可将pi添加到(xy)作为条件命题,且约束x、y在此命题列的真值取值分别为1、0.(3)插入规则.如果pi→pi',可将p’与p’插入到(xy)作为条件命题,且约束x、y在pi命题列的真值取值分别为1、0,而在p命题列的真值取值分别为0、1.类似地,结论命题q、q也遵循上述3条规则添加到(xy)之中,由此生成的合并真值表最多包含组件约束x、y的所有条件、结论命题,命题公式个数不超过m+n,并含有2行真值取值序列,每行表示1条组件约束,即真值指派序列为组件约束的个数.同样,遵循上述规则,合并n条组件约束x1,…,xn,可以得到合并真值表的形式化表示,描述如下.23冗余与冲突的检测x,y为2条约束,(x)=(p1,…,pm,q),(y)=(p1’,,pn’,q’),其中p1,…,pm为x约束的条件命题,q为结论命题,p1’,…,pn’和q’分别为y约束的条件与结论命题,合并的真值表(xy)的指派序列(xy)满足如下定理.证明合并的真值表提供了一系列的组合,它可扩展为一系列组件约束,同时提供一种冲突与冗余的检测方式.在合并的真值表中,真值指派行表示组件约束,列表示原子命题.显然,在条件命题逻辑原子公式集合中,所有的列都有相同的真值,但却收集了不同行,这意味着结论冲突.如果在结论命题逻辑原子公式集合中所有的列的真值均相同,但收集了不同行,则为前提冲突;如果不同行的所有列项一致,则为冗余的情况.总之,异常的情况是指:在合并的真值表中真值有共同的列,以及在同一个列中占据不同的行.冗余与冲突的检测算法如图1所示.3实验结果及分析通过分析业务流程中的控制流信息,将整个业务流程中的所有数据访问操作组成的数据访问序列称为数据访问流,用带权有向图表示.数据访问节点的权值规定如下:并行、选择、序列活动的权值为1,重复活动的权值为重复的次数.有向边的权值规定如下:序列、并行、重复控制结构中的边,权值为1,选择控制结构中的边,权值为该边可能被执行的概率.图2为一个数据访问流的例子.数据访问流可以通过对业务流程进行如下处理得到:删除流程中所有的非数据访问节点;根据活动的控制结构,确定每个活动节点的执行次数,并作为该活动在数据访问流中的权值;指定数据访问节点的操作类型、操作要求.因此,通过业务分析,可以找到数据访问节点之间的约束关系,再将数据访问节点映射成数据访问组件.选取U-Rent的用例,可以找到500条组件约束,分别采用基于命题逻辑和基于规则模式表的方法进行实验,通过运行测试比较了这2种检测方法的性能,结果如表2所示.其中,错判率是检测出错的约束与所有检测到的约束之比,漏判率是未能检测出问题的约束与所有的约束之比.\通过实验结果可以得出,对于组件约束的冗余与冲突的检测情况,命题逻辑的方法能降低冲突错判率,而且极大地改善了检测处理的时间性能,平均处理时间要比规则模式表方法降低33%.4结论最少无冲突的组件约束集可以客观、准确地描述软件系统,包括软件组织结构、动态行为以及组件之间的转换.本文提出了一种基于命题逻辑的检验方法,并利用它进行组件约束的冲突与冗余检验.该方法可以全面描述组件约束以及异常类型,改善检测的时间性能,降低异常检测的错判率与漏判率,这对于提高软件的可靠性和稳定性意义重大.致谢感谢IBM中国研究中心提供试验软件和大量相关技术文献和资料,感谢IBM中国研究中心组件部门张冠群先生提供的有益建议.参考文献:[1]CrnkovicI,LarssonM.Challengesofcomponentbaseddevelopment.TheJournalofSystemsandSoftware,2002,61:201212.[2]MeiHong,ChengFeng,FengYaodong,etal.ABC:anarchitecturebased,componentorientedapproachtosoftwaredevelopment[J].JournalofSoftware,200