多代理系统架构的形式建模与验证

0AASRI Procedia  5 ( 2013 )  126 – 13202212-6716 © 2013 年该作者发表，由 Elsevier B.V.发表。由美国应用科学研究学会负责选择和/或同行评审。doi: 10.1016/j.aasri.2013.10.0680ScienceDirect02013 年并行与分布式计算系统 AASRI 会议0多智能体系统的形式建模和验证0架构0a 樱花科技大学计算机科学学院0a 华中科技大学计算机科学学院0b 湖北科技学院计算机科学学院0摘要0在多智能体系统中，多个分布式智能体相互交互以解决问题。为了指导多智能体系统的开发，多智能体系统架构将提供一个框架。具体的多智能体系统可以从多智能体系统架构中定制，无需重新编写构造。为了满足多智能体系统的故障恢复属性，我们提出了带有容错机制的可靠多智能体系统架构。使用 PVS 形式语言构建系统架构，可以为系统开发人员提供常见模式和习语。为了满足可靠性要求，可以使用强大的 PVS定理证明器来分析所提出架构的高可靠性属性。© 2013 年由 Elsevier B.V.发表。由美国应用科学研究学会负责选择和/或同行评审。关键词：形式建模；形式验证；多智能体；系统架构；定理证明器；容错01. 引言0多智能体系统是由多个互动智能体组成的系统 [1]。当解决问题时，如果使用单个智能体很难解决，我们就会使用多智能体系统。0在多智能体系统中，通过多个分布式智能体相互交互来解决问题。为了指导多智能体系统的开发，多智能体系统架构将提供一个框架。具体的多智能体系统可以从多智能体系统架构中定制，无需重新编写构造。为了满足多智能体系统的故障恢复属性，我们提出了带有容错机制的可靠多智能体系统架构。使用 PVS 形式语言构建系统架构，可以为系统开发人员提供常见模式和习语。为了满足可靠性要求，可以使用强大的 PVS 定理证明器来分析所提出架构的高可靠性属性。0*  通讯作者：手机号：86-18986636933。电子邮件地址：fanping1028@126.com。0在 www.sciencedirect.com 上在线提供0© 2013 年该作者发表，由 Elsevier B.V. 发表。由评审。0根据 CC BY-NC-ND 许可协议进行开放访问。0根据 CC BY-NC-ND 许可协议进行开放访问。 0127  Ling Yuan 和 Ping Fan /  AASRI Procedia  5 ( 2013 )  126 – 1320在线交易、灾难响应和建模社会结构等领域，由于软件架构是减轻分布式系统开发复杂性的很好选择[2]，[3]，我们将架构风格应用于多智能体系统的开发中。由于这些种类的多智能体系统应用在构建层面上具有共同性，多智能体系统架构 (MASA)在开发多智能体系统方面非常有帮助。多智能体系统也倾向于快速自我恢复以满足可靠性要求。在提出的 MASA中，融入了容错机制 [4]，[5]，以为多智能体系统提供异常处理能力。借助明确定义的语义，可以使用形式方法[6]，[7] 来编写精确的规范并处理对架构设计的严格验证。原型验证系统 (PVS) [8]，[9]在编写形式语言和处理复杂高可靠性系统的验证方面非常强大。PVS 的形式语言易于学习如何指定模型。PVS的定理证明器可以通过用户输入证明引理来控制。PVS的这些优势对于验证多智能体系统架构是否能满足高可靠性要求非常有帮助。本文的剩余部分组织如下。第2节描述了 PVS 的基本概念。第3节说明了 MASA 的结构。第4节描述了 MASA 的 PVS 规范模型。第5节演示了MASA 的模型是否能满足高可靠性要求。第6节对本文进行了总结。02. 背景-原型验证系统0在原型验证系统 (PVS)中，形式规范通常由理论组成。如图1所示，我们使用一个列表示例来解释如何编写一个理论。LIST THEORY有一个参数 Entry。这里有两个重要的函数。Leave 函数指定旧条目如何离开列表。Join函数指定列表如何接收新条目。0图1 LIST 理论示例0在验证过程中，PVS定理证明器可以构建一个证明树，其中所有的节点都应为真。证明树的节点可以被视为一个推理。推理由前提和结论组成。例如，在前提中可以找到 A1 和 A2，在结论中可以找到 B1 和 B2，如图2所示。通过输入 PVS证明命令，PVS 定理证明器可以处理验证。0图2 PVS 定理证明器的证明树0LIST [Entry. Type+]:THEORY  BEGIN     entries: TYPE=[#size: nat, elements:ARRAY[{i|iEntry]#]     ents: VAR entries     nonemptylist?(ents): bool=(size(entries)>0)nents: 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|iMSG]0send data[[BASTATE,[PORT->AMSG]] ->[BASTATE]]0except_context:[EXCEPT->EH]0except_handle:[EH->SRSTATE]0Send: TYPE=[#inter_state: BASTATE, checkpoint:SRSTAET,ue_re:SIG#]0sd:VAR Send0SendData (sd):Send=IF member(inter_state(ts), n_states) THEN(#inter_state:=PROJ)_1(senddata0(inter_state(sd),(LAMBDA p:dc_msg(p)))), checkpoint:=inter_state(sd), ue_rec:=0 #)0ExceptProp agate (sr):BASTATE=Ifmember(inter_state(sd),0excepts)AND ue_rec(sd)=0 THEN inter_state(sd)0ftap:VAR FTA0UniExceptReceive (sd, ftap):Send=IF uni_exception=0Except_graph(exceptions(ExceptRec(ftap))) THEN (#inter_state:=uni_exception,0checkpoint:= checkpoint(sd),ue_rec:=1#)0UniExceptHandle (sd):Send=0IF member(inter_state(sd), excepts)AND ue_rec(sd) =1 THEN (IF member(except_handle0(except_context(inter_state(sd))),n_states)THEN0(#inter_state:=except_handle(except_context(inter_state(sd))),checkpoint:= inter_state(sd),0ue_rec:=0#)ELS IF0except_handle(except_context(inter_state(sd)))=Fail0THEN (#inter_state:=Fail, checkpoint:= inter_state(sd), ue_rec:=0#)0END BA 0130     Ling Yuan and Ping Fan /  AASRI Procedia  5 ( 2013 )  126 – 1320异常处理策略可以是协调错误恢复机制。FTA理论如图5所示.0图5  FTA理论0在FTA理论中，有两个重要的函数. 一个函数ExceptRec说明当引发全局异常时，异常处理代理应该接收此异常.函数ExceptGraph指定了当接收到一组全局异常时，这些异常可以解析为一个全局异常.并且这个解析后的异常应该由异常处理代理处理.05. 使用PVS验证MASA0使用MASA的PVS形式模型，PVS定理证明器可以在验证MASA的容错性质方面非常有帮助.05.1. 引发异常0在本节中，我们说明了MASA如何处理引发的异常.这个容错性质inode_pred1表示当共享资源组件INode引发异常Inodettacked时，分布式代理（例如BA）应该接收这个引发的异常，并处理它，如图6所示. 图6展示了PVS定理证明器的工作方式.当定理证明器提示一个提示Rule?时，用户可以发送一个证明命令. 例如，证明命令可以是flatten.这个命令用于解决分离式联结，并将结论inode_pred1转化为一个序列.0图6 规则输入0FTA:THEORY  BEGIN  IMPORTING G Generic Type, List[EXCEPTION]except_graph:[items[EXCEPTION]-> EXCEPTION]  exception: EXCEPTION  FTA:TYPE=[#exceptions: items[EXCEPTION], uni_exception: EXCEPTION#]  fta: VAR FTA  emptyfta:FTA=(#exceptions:=empty,uni_exception:=e#)  ExceptRec (fta):FTA=(#exceptions:=join(exception, exceptions(oc)), uni_exception: exception#)  ExceptGraph(fta):FTA=    IF exceptions(ExceptRec(fta))/= empty     THEN(#exceptions:=empty,uni_exception= except_graph(exceptions(ExceptRec(fta)))#)     ELSEemptyfta  END IF0inode_pred1: |------  {1}(EXISIS(ba:BA):member(inter_state(sd), excepts)ANDue_rec(sd)=0) IMPLIES (FORALL(qa:QA),(ftap:FTA):Inter_state(UniExceptReceive(dc,ftap))=except_graph(exceptions(ExceptRec(ftap))))Rule?:(flatten) tsft_pred1: {-1}(EXISIS(ba:BA):member(inter_state(sd), excepts)ANDue_rec(sd)=0) |------ {-1}(FORALL(qa:QA),(ftap:FTA):Inter_state(UniExceptReceive(dc,ftap))=except_graph(exceptions(ExceptRec(ftap))))Rule?: 0131  Ling Yuan and Ping Fan /  AASRI Procedia  5 ( 2013 )  126 – 13205.2. 在PVS中验证容错性质0如图7所示，属性inode_pred1的证明脚本由PVS的定理证明器从用户接收到的所有证明命令组成.这些证明命令包括flatten, skolem! , asset等. 证明命令的解释可以在PVS工具手册中查阅.例如，flatten用于使用常量替换前件中的量化变量.0图7 证明脚本0在证明脚本中，除了这些原始引理之外，还有其他重要的引导引理.当验证结果不为真时，这些引理可以指导验证过程. 例如，在NonEmpty引理中指示了异常列表不为空.从UniExceptReceive函数引发异常时，该异常处理组件接收异常的方式在ExceptGraph1中指明.在验证容错性质时，可以将证明脚本直接输入PVS定理证明器. 然后，容错性质可以自动验证.除了这个容错性质，我们还可以成功验证其他性质.06. 结论0本文提出了一个多主体系统架构（MASA）来帮助开发复杂的多主体系统.为了使这个提出的MASA更加精确，我们使用PVS的形式语言来指定MASA.使用MASA的PVS形式模型，强大的PVS定理证明器可以帮助验证高可靠性要求.0致谢0作者们要感谢国家自然科学基金（No. 61100059）的赞助支持.湖北省自然科学基金在拨款2012FFB00901下的大力支持，湖北省教育厅科学技术研究项目在拨款D20132803下的大力支持，湖北科技学院博士启动基金在拨款BK1204下的大力支持，湖北科技学院教学研究项目在拨款2012X016B下的大力支持，咸宁市科学技术研究项目在拨款XNKJ-1203下的大力支持.0(展开)(斯科莱姆！)(引理“传播”)(断言)(斯科莱姆！)(实例化-1(“ba!1”))(断言)(属性)(隐藏-2)(隐藏-2)(引理“传播”)(断言)(斯科莱姆！)(实例化-1(“coc!1”))(断言)(属性)(隐藏-3)(隐藏-3)(引理“异常传播”)(实例化-1(“pc!1”))(替换-1(-1-3)rl)(隐藏-1)(引理“非空”)(实例化-1(“ccp!1”“pc!1”))(引理“CCReceive”)(实例化-1(“ccp!1”))(断言)(引理“异常图1”)(实例化-1(“ccp!1”“qa!1”))(替换-1(-1-2)rl)(隐藏-1)(引理“UniExcept”)(实例化-1(“ccp!1”“dc!1”))(属性)(引理“异常图1”)(实例化-1(“ccp!1”“crr!1”))(替换-1(-1-2)rl)(隐藏-1)(引理“UniExcept”)(实例化-1(“ccp!1” “ccr!1”))(属性) 0132     凌远和平凡/ AASRI Procedia  5 ( 2013 )  126 – 1320参考文献0[1] Michael Wooldridge, “多代理系统导论”, John Wiley & Sons Ltd, 2002. [2] G.T.Leavens和M.Sitaraman.基于组件的系统基础. Cambridge University Press, 2000.  [3] M.Shaw和D.Garlan, “软件架构: 新兴学科的视角”,Prentice Hall, 1996.  [4] G.D.Abowd, R.Allen和D.Garlan. 形式化样式以理解软件架构描述. ACM  Transactions onSoftware Engineering and Methodology, 1995, vol4(4): 319-364.  [5] P. Clements，D. Garlan，L. Bass和J. Stafford.文档化软件架构: 视图及其他. Pearson  Education, 2002.  [6] L.Yuan, J.S.Dong, J.Sun和H.A.Basit.通用容错软件架构推理与定制化.  IEEE Transactions on Reliability, 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 Computer SocietyPress,  2006:209-216.  [9] J. Xu, A. Romanovsky和R. Campbell. 分布式对象系统中的异常处理和解决方案. IEEETransactions on Parallel and Distributed Systems, 2000, 11(10): 1019-1032.