2013年AASRI多Agent系统体系结构形式化验证及PVS定理证明器的应用

© 2013由Elsevier B.V.发布由美国应用科学研究所负责选择和/或同行评审可在www.sciencedirect.com在线获取ScienceDirectAASRI Procedia 5（2013）126 - 1322013年AASRI并行和分布式计算系统多Agent系统体系结构的形式化建模与验证凌源a，范平b*a华中科技大学计算机科学学院，中国b湖北科技大学计算机学院，湖北，中国摘要在多智能体系统中，多个分布式智能体相互交互以解决问题。多智能体系统体系结构为多智能体系统的开发提供了一个框架。具体的多智能体系统可以从多智能体系统的体系结构中定制，不需要重新构造。为了满足多智能体系统的故障恢复特性，提出了一种具有容错机制的可信多智能体系统结构。PVS形式化语言用于构建系统体系结构，为系统开发人员提供通用的模式和习惯用法。为了满足可靠性要求，可以使用功能强大的PVS定理证明器来分析所提出的架构的高可靠性属性。© 2013作者。由Elsevier B. V.在CC BY-NC-ND许可下开放获取。由美国应用科学研究所负责选择和/或同行评审关键词：形式化建模;形式化验证;多智能体;系统体系结构;定理证明器;容错1. 介绍多智能体系统是由多个相互作用的智能体组成的系统[1]。当单个智能体难以解决问题时，我们使用多智能体系统。这些问题可能*通讯作者：手机：18986636933。邮箱：fanping1028@126.com2212-6716 © 2013作者由Elsevier B. V.在CC BY-NC-ND许可下开放获取。美国应用科学研究所负责的选择和/或同行评审doi：10.1016/j.aasri.2013.10.068Ling Yuan and Ping Fan/AASRI Procedia 5（2013）126127由于软件体系结构是减轻分布式系统开发复杂性的很好选择[2]，[3]，我们将体系结构风格应用于多智能体系统的开发。由于这类多Agent系统应用在构造层次上具有共性，因此多Agent系统体系结构（MASA）对多Agent系统的开发具有重要的指导意义。多智能体系统也往往是快速自我恢复，以满足可靠性要求。在所提出的MASA中，引入了容错机制[4]，[5]来为多代理系统提供异常处理能力。有了定义良好的语义，形式化方法[6]、[7]就可以为体系结构设计编写精确的规格说明并进行严格的验证。原型验证系统（Prototype Verification System，PVS）[8]、[9]在编写形式化语言和处理复杂高可靠性系统的验证方面非常强大。PVS的形式化语言易于学习如何指定模型。PVS的定理证明器可以由用户通过输入证明引理来控制。PVS的这些优点有助于验证多Agent系统体系结构是否能够满足高可靠性的要求。本文的其余部分组织如下。第2节描述了PVS的基本概念。MASA的结构见第3节。MASA的PVS规范模型在第4节中描述。第五节论证了MASA模型是否满足高可靠性要求。第六节是对全文的总结。2. 背景-原型验证系统在原型验证系统（PVS）中，形式规格说明通常由理论组成。如图1所示，用一个列表例子来说明如何写一个理论。列表理论有一个参数Entry。这里有两个重要的功能。一个函数Leave指定旧条目如何离开列表。函数Join指定列表如何接收新条目。[入口]类型+]：理论开始条目：TYPE=[#size：nat，elements：ARRAY[{i| i< size}->Entry]#] ents：VAR条目非空列表？（ents）：bool=（size（entries）>0）ents：VAR（nonemptylist？）join（entry，ents）：entries=（#size：=size（ents）+1，elements：= elements（ents）WITH[（size（ents））：=entry]#）leave（entry，nents）：entries=（#size（nents）-1，）entries：=（LAMBDA（j：{ i| i< size（nents）-1}：elements（nents）（j+1））#）END队列图1 LIST理论在验证过程中，PVS定理证明器可以构造一个证明树，其中所有节点都应该为真。证明树的节点可以被认为是一个节点。前件由前件和后件组成。例如，A1和A2可以在先行词中找到，B1和B2可以在后件中找到，如图2所示。通过输入PVS证明命令，PVS定理证明器可以处理验证。图2 PVS定理证明器128Ling Yuan and Ping Fan/AASRI Procedia 5（2013）1263. 多Agent系统结构在这一部分中，我们描述了多Agent系统体系结构（MASA）的体系结构风格。如图3所示，MASA中的分布式代理：代理代理（BA）、查询代理（QA）、查询工具代理（QTA）、通信代理（CA）和监控代理（MA）;共享资源：信息节点（INode）;容错代理：FTA;以及连接器：BtoQ、QtoB、CtoB、BtoC、QtoQT、QTtoQ、BtoQ和QtoB。图3多Agent系统结构分布式代理可以彼此交互以完成作业。信息资源全部存储在信息节点中。两个代理通过使用连接器相互通信。当系统中出现异常时，容错代理负责处理它们。QA和BA相互交互以传递接口查询。QA负责决定是否寻找其他BA。BA负责决定哪个INode拥有相关信息。QTA负责代理商之间的沟通。MA处于控制位置，其工作包括构建QA以设置查询、接收查询结果并分析结果。CA负责搜索潜在的项目，分析它们，并选择合适的项目。在体系结构层次上，集成了容错技术来处理异常。在提出异常时，我们应该使用适当的处理策略来处理它，但处理结果可能是假的，然后将此异常传递给容错代理，以全局异常的形式发出信号。全局异常可能会影响其他交互代理。因此，全局异常应该通知相关代理，并且这些代理必须处理被通知的全局异常。4. MASA的PVS形式化模型以容错Agent FTA和分布式Agent BA为例，说明了MASA4.1. BA规格模型BA负责与代理QA交互。当出现异常时，BA可以处理这些异常。BA理论如图4所示。Ling Yuan and Ping Fan/AASRI Procedia 5（2013）126129在BA理论中，有四个重要功能。一个函数是SendData，它用于描述BA如何使用连接器向QA发送信息 。 如 何 将 引 发 的 异 常 传 递 给 异 常 接 收 代 理 ， 在 函 数 Exceptagerate 中 进 行 了 说 明 。 函 数UniExceptReceive说明了如何从异常接收代理接收异常。最后一个函数UniExceptHandle解释BA是否可以成功处理接收到的异常。如果成功的话，内部状态可以正常。否则，状态应指示此代理无法成功处理此异常。BA[BASTATE：TYPE+]：THEORY BEGIN进口FTCn_states，excepts：setof[BASTATE]端口号，tsout_ports：setof[PORT]dc_msg：[PORT->MSG]发送数据[[BASTATE，[PORT->AMSG]]->[BASTATE]]except_context：[EXCEPT->EH]except_handle：[EH->SRSTATE]发送：TYPE=[#inter_state：BASTATE，checkpoint：SRSTAET，ue_re：SIG#] sd：VAR发送SendData（sd）：Send=IF member（inter_state（ts），n_states）THEN（#inter_state：=PROJ）_1（senddata（inter_state（sd），（LAMBDA p：dc_msg（p），checkpoint：=inter_state（sd），ue_rec：=0 #）ExceptProp agate（sr）：BASTATE=Ifmember（inter_state（sd），excepts）AND ue_rec（sd）=0 THENinter_state（sd）ftap：VAR FTAUniExceptReceive（sd，ftap）：Send=IF uni_exception= Except_graph（exceptions（ExceptRec（ftap）THEN（#inter_state：=uni_exception，checkpoint：= checkpoint（sd），ue_rec：=1#）UniExceptHandle（sd）：发送=IF member（inter_state（sd），excepts）AND ue_rec（sd）=1 THEN（IF member（except_handle（except_context（inter_state（sd），n_states）THEN（#inter_state：=except_handle（except_context（inter_state（sd），checkpoint：= inter_state（sd），ue_rec：=0#）ELS IFexcept_handle（except_context（inter_state（sd）=失败THEN（#inter_state：=Fail，checkpoint：= inter_state（sd），ue_rec：=0#）END BA图4 BA理论4.2. FTA的规格模型FTA的规范模型负责说明如何处理全局异常。130Ling Yuan and Ping Fan/AASRI Procedia 5（2013）126异常处理策略可以与错误恢复机制相协调. FTA理论如图5所示。FTA：理论开始IMPORTING G泛型类型，List[EXCEPTION]except_graph：[items[EXCEPTION]->EXCEPTION] exception：EXCEPTIONFTA：TYPE=[# exceptions：items[EXCEPTION]，uni_exception：EXCEPTION#] fta：VAR FTAemptyfta：FTA=（#exceptions：=empty，uni_exception：=e#）ExceptRec（fta）：FTA=（# exceptions：=join（exception，exceptions（oc）），uni_exception：exception#）ExceptGraph（fta）：FTA=IF exceptions（ExceptRec（fta））/=空THEN（#exceptions：=empty，uni_exception= except_graph（exceptions（ExceptRec（fta）#）ELSE emptyftaEND IF图5 FTA理论在自由贸易区理论中，有两个重要的功能。一个函数ExceptRec说明了当引发全局异常时，异常处理代理应该接收该异常。函数ExceptGraph指定当接收到一组全局异常时，这些异常可以被解析为一个全局异常。这个解决的异常应该由异常处理代理处理。5. 使用PVS利用MASA的PVS形式化模型，PVS定理证明器可以很好地验证MASA的容错性。5.1. 引发异常在本节中，我们将演示MASA如何处理引发的异常。该容错属性inode_pred1指示当共享资源组件INode引发异常Inodettacked时，分布式代理（例如BA）应该接收该引发的异常，并处理它，如图6所示。图6显示了PVS的定理证明器是如何工作的。当定理证明器提示一个提示规则？用户可以发送证明命令。例如，proof命令可以是flatten。此命令可用于解析析取连接词，并将结果inode_pred1转换为谓词。inode_pred1：|{1}（EXISIS（ba：BA）：member（inter_state（sd），excepts）AND ue_rec（sd）=0）隐含（FORALL（qa：QA），（ftap：FTA）：Inter_state（UniExceptReceive（dc，ftap））=except_graph（exceptions（ExceptRec（ftap）规则？：（flatten）tsft_pred1：{-1}（EXISIS（ba：BA）：member（inter_state（sd），excepts）AND ue_rec（sd）=0）|{-1}（FORALL（qa：QA），（ftap：FTA）：Inter_state（UniExceptReceive（dc，ftap））=except_graph（exceptions（ExceptRec（ftap）规则？：图6规则输入Ling Yuan and Ping Fan/AASRI Procedia 5（2013）1261315.2. PVS中的容错性验证如图7所示，属性inode_pred1的证明脚本由PVS的定理证明器在验证属性时从用户接收的所有证明命令组成。这些证明命令是扁平的，skolem！、资产等。证明命令的解释可以在PVS工具手册中查阅。例如，flatten用于使用常量来替换先行项中的量化变量。（flatten）（skolem！）（lemma“restricate”）（assert）（skolem！）(ins tantiate-1（“ba！1”））（assert）（prop）（hide-2）（hide-2）（lemma“pronounate”）（assert）（skolem！）(instantiate-1（“coc！11”））（replace-1（-1 - 3）rl）（hide-1）（lemma“NonEmpty”）（instatiate-1（“ccp！1”“pc！1”））（lemma“CCReceive”）（instatiate-1（“ccp！1”））（assert）（lemma“ExceptGraph1”）（instatiate-1（“ccp！1”“qa！1”））（replace-1（-1 -2）rl）（hide-1）（lemma“UniExcept”）（instatiate-1（“ccp！1”“dc！1”））（prop）（lemma”ExceptGraph1”）（instatiate-1（“ccp！1”“crr！1”））（replace-1（-1 - 2）rl）（hide-1）（lemma“UniExcept”）（instatiate-1（“ccp！1”））（prop）图7校对脚本在证明脚本中，除了这些原始引理，还有其他重要的诱导引理。当验证结果不为真时，这些引理可以指导验证过程。例如，在NonEmpty引理中指出异常列表不为空。当从UniExceptReceive函数引发异常时，异常处理组件如何接收异常在ExceptGraph1中指示。在验证容错性质时，证明脚本可以直接输入到PVS定理证明器中。容错性能可以自动验证。除了这种容错性，我们还可以成功地验证其他属性。6. 结论本文提出了一种多智能体系统结构（MASA），以帮助开发复杂的多智能体系统。为了使该算法更加精确，我们使用PVS形式化语言来描述MASA。利用MASA的PVS形式化模型，功能强大的PVS定理证明器可以帮助验证高可靠性要求。确认作者感谢国家自然科学基金（No.61100059）的资助。在湖北省国家自然科学基金项目2012 FFB00901、湖北省教育厅科技攻关项目D20132803、湖北科技大学博士点启动基金项目BK 1204、湖北科技大学教学研究项目2012 X 016 B的大力支持下，咸宁市科学技术研究项目XNKJ-1203。132Ling Yuan and Ping Fan/AASRI Procedia 5（2013）126引用[1] 陈文生，[2] 作者声明：Dr.基于代理的系统的基础。剑桥大学出版社，2000年。[3] 肖先生和加兰先生，[4] 作者声明：by G.D.形式化风格以理解软件体系结构的描述。ACM软件工程与方法学报，1995，第4卷（4）：319-364。[5] P. Clements，D.加兰湖巴斯和J·斯塔福德文档化软件架构：视图和超越。Pearson Education，2002.[6] L.Yuan，J.S.Dong，J.Sun，和H.A.Basit.通用容错软件体系结构推理和定制。IEEE Transactions onReliability，2006 55（3）：421-435.[7] J.C.Laprie.可靠性.基本概念和术语独立计算和容错系统。Springer-Verlag，1992.[8] L.Yuan，J.S.Dong和J.Sun。基于Object-Z/XVCL的容错体系结构建模与定制。第13届亚太软件工程会议（APSEC'06）。IEEE计算机协会出版社，2006：209-216。[9] J. Xu，A. Romanovsky和R.坎贝尔分布式对象系统中的异常处理和解决。并行与分布式系统学报，2000，11（10）：1019-1032.