理论计算机科学电子笔记184（2007）189-207www.elsevier.com/locate/entcs面向数据库的形式化分析--以协议和分布式系统为Carlos Bazilio1 Edward Hermann Haeusler2DepartametodeInformicaPUC-Rio巴西里约热内卢摘要本文的主要动机是描述一种架构，旨在通过模型检查简化分布式算法和协议（可能是移动的）的验证。该体系结构的核心是协议规范语言（LEP），它具有称为代词的结构，允许高级级别规格。这意味着与我们实验中使用的模型检查器的通用规范语言相比，规范要少得多。通过两步过程，LEP规范被翻译成模型检查器的语言，结果被翻译回LEP。 在翻译过程中使用了一个正式的通信模型，以允许使用不同的模型检查器。目前，该架构的原型使用模型检查器Spin和SMV。保留字：协议规范，形式验证，模型检查。1介绍由于当前大多数系统所固有的巨大复杂性，验证系统的任务变得越来越困难。当系统是分布式的或具有移动元素时，这些困难甚至更大。对于这些系统，支持验证的技术和自动化工具，如模拟，等价性检查，定理证明和模型检查甚至更加重要。上述工具和技术在系统开发和验证中的应用被称为系统的形式化分析。本文主要讨论分布式算法和协议的形式化分析。在续集中，我们讨论，在认识论的基础上，形式化方法（主要是模型检查MC）作为软件测试的主要扩展的重要用途1电子邮件地址：bazilio@inf.puc-rio.br2电子邮件地址：hermann@inf.puc-rio.br3电子邮件地址：endler@inf.puc-rio.br1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.03.022190C. Bazilio等人/理论计算机科学电子笔记184（2007）189面向语言的软件开发（LOSD）是一种形式化的软件系统开发技术，它基于一种语言的（形式）语义所构建的工具的应用，该语言被设计得足够强大，以描述与之相关的特定领域。LOSD的成功和代表性例子是数据库系统和编译器构造。前者是基于关系演算和SQL变量，而后者是基于正式的语义，如SOS，动作语义和指称语义，除了语法的解析器的建设。通过提供适当的语言及其形式语义，人们可以自动地为程序设计语言开发调试器甚至可视化环境。在70年代和80年代，编译器和DBML得到了很大的形式方法社区所倡导的主要优点之一是以这种方式开发的软件的正确性一般的论点是，从一个（正确的）规范中，人们（自动地）导出正确的运行代码。我们不会遵循这一论点。相反，我们认为使用形式方法的主要优点是，一般来说，它们基于具有精确语义的语言，并且大多数时候这种语义非常适合特定领域。我们采用了科学理论和软件系统的发展之间的类比，这是Haeberer和Maibaum很好地处理的（读者可以阅读[12]作为软件工程师非常有用的观点的例子）。根据认识论和科学论的主要思想，科学理论的验证是不可行的。继波普尔之后，科学通过反驳和反驳的循环而发展。这个循环的必然存在来自于科学理论固有的可证伪性原则。就其结构而言，一个科学理论是由理论术语和经验术语构成的，它们分别由构成该理论的语言装置的理论语言和经验语言构成。卡尔纳普[4]对科学理论进行了语言学分析，这在科学理论开发和软件系统开发之间进行类比时非常有用。粗略地说，他的分析得出结论，虽然理论的理论定律，用理论语言表述，本质上是普遍的，但可观察实验本质上是存在的。也就是说，用实验的方法检验一个理论规律，不能“根据理论的规律，必然要求这个假设是正确的”。诚实的说法是从形式上讲，卡尔纳普主张，对科学理论的分析是在理论语言所表达的理论规律的背景下进行的，这是一个在理论的经验（可观察）语言的帮助下制定的假设，并且有一个支持对假设进行评价的背景理论。卡尔纳普从上面讨论的和已经建立的科学理论和软件开发之间的类比，我们主张软件开发的过程C. Bazilio等人/理论计算机科学电子笔记184（2007）189191系统的构建应以卡尔纳普的语言学框架为基础，以系统的实用性为目标。根据上述分析，软件的正确性是不可达到的。从一个天真的观点来看，除非一个形式化的具体化显然是形式定理证明的任务不能被认为是逃避这种情况的一种方式，因为，关于系统的要证明的陈述并不是整个系统的属性集，根据莱布尼茨原理，它标识了它。为了提供一个软件系统（形式）分析的平台，以便开发出有用的软件，我们遵循Carnapian语言学的科学观，提出了面向语言的软件开发（LanguageOriented事实上，这种方法本身不能说是一种新颖的方法，因为在我们之前，它已经在许多公认的领域中得到应用。本文的主要目的是展示一个案例研究，一个基于语言的分布式算法和协议规范化与形式化分析的体系结构。我们的主要贡献是对这个问题的明确陈述，以及应用统一语言为规范的理论和经验术语提供语义通过在经验和理论（子）语言之间提供较小的语义间隙来确保一致性。这个任务对于我们的案例研究来说特别有趣，因为代词的语言学概念将从分布式算法/协议的角度映射到共性，以及从特定的随着时间的发展，其他共相将在理论上被描述为属性（共相），在经验上被描述为反例。这最后一种情况与形式方法社区没有什么不同;然而，我们的架构将提供规范和普遍概念之间的统一对应，以及支持它们可证伪性的反例。从模型检查器或其他形式化工具提供的痕迹（反例）到非常普遍的语言概念的映射，该语言概念表示产生痕迹的属性中的时间演变，由规范的其余部分诱导，是由建筑提供的。有大量的形式化技术和语言可以帮助SE执行（形式化）分析。在上述形式化分析技术中，MC是一种自动形式化方法，通过彻底探索他们的计算树。这些模型是有限跃迁系统，并与Kripke模型密切相关因此，要验证的属性通常使用时态逻辑来表示然后，模型检查器通常会验证给定的一组属性是否适用于系统的模型与定理证明相比，它具有补充作用后者的目的是建立一个特定的属性是系统/协议/分布式算法的指定的逻辑结果。当然，当这样的性质不是具体化的逻辑/演绎结果时，定理证明器根本没有帮助。 我们主张MC是一个更好的工具，形式化分析比定理证明器，是后来提供函数证明的优秀工具通常在形式分析阶段之后产生。 当然可以用192C. Bazilio等人/理论计算机科学电子笔记184（2007）189然而，为了进行形式分析，通过TP来细化由错误发现提供的规范的任务是困难的我们基于语言的架构旨在通过模型检查简化分布式算法和协议的规范和该架构的核心是协议规范语言（LEP），它具有称为代词的结构，可以进行高级规范。这意味着与我们实验中使用的模型检查器的通用规范语言通过两步过程，LEP规范被翻译成模型检查器的语言在转换过程中，在通信模型的级别上使用了一个中间规范，以便允许使用不同的模型检查器。目前，该架构的原型正在开发中，将模型检查器Spin [10]和SMV [6]作为备选后端。通信模型，在操作语义中正式指定，旨在足够通用，以便能够表示任何协议，无论是否移动。它基于一个（动态）可配置的连接图，该图表示协议中每个功能元素相对于整个网络的每个元素都有一个内部行为，由一个转换系统和队列来管理网络元素之间的任何形式的通信这将在文章的相应部分得到更好的解释在使用原型进行的实验中，DSR（动态源路由-ad-hoc网络协议）[11]在这里给出一些方面，例如在该协议的手动规范中发现的规范的大小和复杂性，促使我们提出该架构。对该体系结构进行的实验分析表明，使用代词作为Carnapian意义上的理论语言的普遍性与经验语言的存在性之间的桥梁，是实现分布式算法和协议分析的有用平台的强大语言组成部分。值得一提的是，使用Net-Grammar [7]以及模态时间逻辑的过滤来改进搜索空间探索，在时间方面，以理论上合适的方式进行（时间）属性的分析也就是说，对网络拓扑的一大类实例的性质的验证是在有限的实例集上以合理和完整的方式进行的。由于篇幅有限，本文没有详细说明，但提及这一点是为了指出案例研究的统一性问题。该体系结构并不打算通过模型检查技术来解决所谓的这是一个难题。除了已知MC中常用的时态命题逻辑（即CTL、LTL和μ-演算）的可判定性问题从PSPACE-完备到EXPTime-完备都是困难的之外，还证明了指数大小规格（与有效属性的大小相比）与CoNP复杂性类密切相关，通过从经典命题证明到过渡系统上的时间属性的映射，如C. Bazilio等人/理论计算机科学电子笔记184（2007）189193也与SAT求解器（NP复杂性类）密切相关。因此，系统的组合验证的一般模式的可行性似乎是很难解决的类NP，CoNP和PSPace的主要命题。当然，从时态逻辑的复杂性来看，似乎可以得出结论，这可能是一个不可行的任务，因为类EXPTime独立于已经提到的主要结构。因此，我们的架构旨在更广泛地使用MC技术，通过在后端允许几个工具，这当然是一个可行的任务。2建议的体系结构这种架构可以被看作是通常模型检查过程之上的附加层。它应该简化验证过程，因为它的领域特定语言对用户透明，所选模型检查器的特定语言的细节2.1一般描述图1描述了建议的架构。顶层由LEP（协议描述加上要检查的属性）和模型检查器在协议的原始LEP规范级别上的结果组成。底层包含传统的模型检查过程。 这一层的输入是中间层的输出，中间层进行代码翻译，以便将LEP中提供的规范转换为模型检查器接受的规范。这些到模型检查器语言的翻译是由所选模型检查器特定的模块（图1中的CI2SMV和CI2Spin）完成的。中间层还将模型检查器这个中间层很重要，因为不同的模型检查工具可以互换使用在我们的原型中，所有的翻译器模块都是使用TXL转换语言[8]实现的，它的描述不在本文的范围内。然而，在章节2.4和2.5定义了它是如何工作的。2.2LEPLEP是一种基于进程的语言，例如CCS [14]，用于指定移动协议和分布式算法。它结合了CCS中的守护命令、Pi演算中的名称重载[15]和代词（改编自OO关注点[9]）的概念。代词可以被看作是引用一组元素的一般手段，使规范更短，更清晰和精确。例如，在一个普通的规范语言中，如果我们想向多个进程发送一条消息，我们必须遍历元素集。使用LEP，我们只需书写：代词everyone也适用于部分连接的网络，各位！MSG194C. Bazilio等人/理论计算机科学电子笔记184（2007）189CI2SpinCI2SMV中间代码（CI）高级别模型检查器属性协议CI2LEPLEP2CI中间代码（CI）. . .Fig. 1. 架构广播通信通过消息的广播4如果这个亲名词用于接收信息（每个人？x），则它表现得像将从网络的每个元件接收消息x的同步点。由于我们可能会断开连接，执行此命令的进程可能会无限等待。为了减轻它，我们可以在接收子句中使用代词any（k），等待来自k跳的消息。在LEP中，代词可以出现在元素的标识符可以出现的任何地方。我们考虑以下代词：this：对它出现的同一模块实例的引用;当用作右侧值时，认为是标识该元素的内部（对用户不可见）值;sender：在接收命令的动作子句中，这个代词认为是发送消息的元素;这在请求-应答通信风格中很有用;any（t，k）：这是一个参数和通用代词，引用类型为t的系统中的任何k个元素（不包括它出现的元素）;这个代词将非确定性添加到指定中;anyother（t，x，k）：这是一个参数和通用代词，返回任何k网络中与给定参数x不同的t类型元素;everyone（t）：在发送中，它涉及类型t的每个元素，该元素可以从它出现的元素到达;它可以用于广播和相应的应答消息。在接收消息时，它等待网络中每个元素的消息;neighbors（t，k）：指可到达的t在k步中（从这个节点到目标的路径最多有k个节点）;父节点：关注代词出现的元素的创建者;children：关注代词出现的元素所创建的所有元素。参数k在省略时具有等于1的默认值。 参数t也是可选的，定义代词所考虑的元素类型（模块的标识符）。当省略时，t具有当前模块的类型。关于拓扑，我们扩展了图文法的概念[7]，4当收到信息的主人按顺序 以覆盖整个网络。MC2CI结果下级C. Bazilio等人/理论计算机科学电子笔记184（2007）189195用于定义代词的属性。文法定义了一个规范所采用的拓扑，文法生成的字符串是验证初始状态下拓扑代词通过合成和继承的属性初始化，这些属性在网络生成期间计算，即，属性图文法产生式规则的应用。在属性图语法中插入新的属性是创建用户定义的代词的一种方法。在表1中，我们展示了一种使用属性图文法指定环形拓扑的方法。在这里，我们通过使用属性s-neigh和h-neigh分别为合成和继承属性定义代词邻居在过程结束时，代词邻居由每个生成的节点的属性s-neigh给出在这种情况下：S和S连接非终结符与其右侧;in和out决定输入，规则中的图形语法的输出节点;{和}之间的赋值涉及属性，而外部的元素和有向箭头（←，→，Participate）涉及图形语法。St{t.s-neigh<$S0 ut（S' 2）{ S ' 2. h-neigh←S' 1. h-neigh}S表1基于属性图文法在该架构中，我们为环、星、树、序列、任意和完全图（网络）提供了预定义的语法。此外，我们可以明确地指定初始网络。为了说明LEP中的具体化，图2显示了如何在任意拓扑中指定Leader Election算法。粗体是LEP的保留词，斜体是代词。LEP的特定单元具有定义网络的初始结构的拓扑声明以及模块的声明。拓扑可以是预定义的拓扑，也可以由用户给定。在图2中，标记为1的节点有邻居（节点直接连接）2和3，节点2有1，3和4，等等。关于拓扑当链路和节点没有故障时，拓扑是可靠的，消息不会在系统中丢失。安全意味着消息没有损坏。定向意味着网络中的链接是双向的。当拓扑结构是动态的时，主机的移动是自动进行的，并且对用户透明。它在建模ad hoc网络时很有用，因为通常移动主机会在没有通知的情况下移动。可靠、定向、安全和静态是拓扑参数的默认值候选模块定义了节点的状态机。init和stop标记分别是将在模块的初始和最终状态下执行的命令。Operatortrue这个词也可以是一个前置条件，它表示它的动作可以196C. Bazilio等人/理论计算机科学电子笔记184（2007）189拓扑是{1-{2，3}，2-{1，3，4}，3-{1，2，4}，4-{2，3}}可靠的;模块候选varmy，p，count：int;init-> count = 0; my =this;neighbors！mysql（mysql，mysql）;这个吗win->stop;这个吗msg（p，count）->if（（p> my）or（（p == my）and（counttopology.size）thencount = count +1;邻居们！mysql（mysql，mysql）;其他if（（p == this）and（count> topology.size））then各位！赢;停止;endif图二. LEP中指定的任意网络中的领导者选举尽可能地执行（非确定性地）。进程的同步并接收“？”。如果我们将图2中拓扑的明确定义替换为<它允许重用不同拓扑的规范，这显示了LEP的一个有趣特性。我们还使用代词来指定模型此外，当公式中出现的标识符不是预定义代词时，它统一了变量的出现。 此外，发送和接收命令还作为子公式：[]（p！活着的（每个人）→<> p？ack（any（k）。然而，在这方面，代词的解释在财产中使用时可能会有一点变化。上面用LTL（线性时间逻辑）表示的属性询问是否总是存在这样一种状态，即进程p向每个其他进程发送活动消息，并最终接收至少k个消息ack。我们考虑以下代词来指定被视为发送或接收消息的命令的属性：everyone：指定是否存在进程发送或接收消息的某些状态网络中的所有其他进程;在发送中，每个人都意味着每个可到达的进程;在接收中，它意味着网络中的每个进程;无：指定发送或接收给定消息的进程没有状态; p！msg（none）在语义上等同于not p！msg; any（k）：其含义与每个人对一个k大小的进程子集的含义相同。2.3LEP通信模型在本节中，我们提出了一个分布式算法的计算模型的形式化描述，这是LEP的执行的基础。事实上，在这一部分中，我们描述了形式化的语义LEP从LEP到它的通信模型的翻译。为了简短而有意义的描述，我们专注于LEP的一个重要片段。为了在SOS [16]中指定LEP的计算模型，我们使用了一个我们称为环境的结构（图3）。它的结构是一个图，其中节点vi表示进程，边aij定义进程之间的可用连接。每个C. Bazilio等人/理论计算机科学电子笔记184（2007）189197v：V rtv：Grfgr1：Grf gr2：Grfgr1gr2：Grfv1：V rt v2：V rt a：边一v1 →v：Grf2gr：Grff：V rt（gr）→元素g：Chan→边：环境节点与包含两个缓冲器Bin和out的逻辑元件相关联，缓冲器Bin和Bout分别用于消息的输入和输出交换。通道将这些元件成对互连。图3.第三章。LEP计算模型的环境当发送消息时，发送方进程将消息放入其输出缓冲器，以便传递到接收方进程的输入缓冲器。 缓冲器的大小和存储消息的方式表明系统的行为。布氏器的大小等于零意味着会合通信。消息存储在缓冲器中，缓冲器可以表现为队列、堆栈甚至简单的集合。除了进程之间的外部通信外，每个进程都有可能改变其状态的内部进程的状态由一组局部变量和两个用于存储输入和输出消息的缓冲器组成。这些状态在系统性质的具体化中很重要。我们认为以 下 句 法 类 别 ： e∈Elem={Id×Buf×Buf×Loc×Trans} ， v∈V rt= 顶 点 集 ，a∈Edge={V rt×V rt}，gr∈Grf=V rt×Edge，ch∈Chan=通道集，env∈Env=环境。LEP的计算模型的抽象语法如下：LEP的计算模型的语义规则可以描述如下：→idaJ，binJ，boutJ，αJ，tJ>（一）→（2）→< id，ch？m（val）|bin，bou t，α，t [x]>→→→（三）→< id，bin，bout，α，insert（a，v2）|t>→（四）→< id，bin，bout t，α，remove（a）|t>→（五）→< id，bin，bout，α，insert（v1）|t>→（六）→< id，bin，bout t，α，remove（v1）|t>→（七）→这些规则和相应的条件和背景是：（1）系统f（v）=A，FJ（v）=AJ，{v1，v1/=v，f（v1）=FJ（v1）}的演化;（2）系统的内部演化，v1b输b在e1v2一名v3env198C. Bazilio等人/理论计算机科学电子笔记184（2007）189→sv1，v2∈gr，f（v1）=A，f（v2）=B，v1→av2∈gr，a∈g（ch）;（3）Synchroniztionrulee{v1，v2}gr，f（v1）= ，v1→av2/∈gr，grJ=gr<${v1a v2};（4）箭头插入{v1，v2}{gr，f（v1）=，v1→av2∈gr，grJ=gr−{v1→av2};（5）Arow移除f（v）= ，v∈gr， f（v1）=e，v1/∈gr，FJ（v1）=e，e∈Elem，grJ=gr{v1};（6）Vertexinsertion{v，v1}→gr，v→av1∈gr，f（v）= ，fJ（v1）=φ，grJ=gr−{v→av1};(7)顶点移除;根据这些规则，操作员|“将第一条消息和其余消息分隔在一个缓冲器中，"。将消息与缓冲器连接起来，t[m（val）/x]是一个λ-抽象，它将考虑到消息m（val）收到了2.4从LEP到其计算模型的转换在本节中，我们在SOS [16]中给出了LEP规范如何通过重写规则转换为其计算模型的规范的正式描述在翻译中，我们根据给定的拓扑结构和上下文（代词出现的地方）将代词映射到它们各自的元素。消息交换仅在中间代码中描述，因为指定一对一通信比代词可以完成的一对多通信更简单。由于篇幅所限，我们给出了LEP的部分形式描述。其余的可以用类似的方式描述。考虑到语言上一节，我们可以添加以下内容：mid∈ MId，t∈ Trans = CExp× Cmd，ce∈CExp ，m∈ Msg，cm∈ Cmd，ch∈ Chan ，top∈ Top ，bool∈ Bool ，connec∈MId→ { MId}。在语义模型中，top是网络的拓扑，st是转换的状态，它包含当前模块函数f：Pron × MId × Top→{ Chan}和g：Chan→ MId × MId提供关于网络拓扑的信息。LEP中的消息被转换为带有两个附加参数的消息，这两个参数可以被视为消息标识符和一个布尔值，指示是否必须像代词everyone中那样转发消息。语义规则如下：C. Bazilio等人/理论计算机科学电子笔记184（2007）189199<拓扑是连接参数; mod prop>Q<$mod，<$processTopology（connections，params，mod））Q，第二：|比因|为|布图|=0，{{vass oc（v）=0}Q<$tlep1，st（中间，顶部））<$tlep2，st（中间，顶部））Q<$celep，st（mid，top））->● generateConditionEveryone（celep，mid，top））<$cmlep，st（中部，顶部））Q<$cmlep1，st（中部，顶部）;<$cmlep2，st（中部，顶部））<如果ce则cm endif，st（ mid，top）>Q如果<$ce，st（ mid，top））{<$ cm，st（ mid，top））}< 邻居们！m，st（ mid，top）>Qreturn0;while（local1<=k）{ch[local1]！mid（mid，false）;local1++;}，nde：proces Pro n（nei ghbou rs，mid，to p）={c h [1]，.，ch[k]}，g（ ch[1]）= mid1，g（ ch[ k]）= midk，{mid1，midk}{ MIdd}，K= |processPronoun（neighbors，mid，top）|翻译规则的条件分别为 （一）|b在|为|= 0，{v_asv（v）}|= 0, {∀v assoc (v)= }; （2）无; （三）无; （四）如果网络是不可靠的即，节点可以丢弃消息（5）g（ch）=（m，mid），m∈MId（7）f（neighbors，mid，top）={ch1，...， ch k}，g（ch1）=（mid，id1），g（ch k）=（mid，id k）id1. k∈ MId，1 ≤ k ≤ |f（邻位，中间，顶部）|. 函数processTopol-ogy生成拓扑信息以便在转换中使用，并且函数generateConditionEveryone生成测试到达的消息是否必须被转发或者已经被接收的命令，并且根据这些条件转发2.5从计算模型到Promela的在本节中，我们将展示架构的中间代码如何映射到Promela（Spin的输入语言）的结构中翻译几乎是直接的，因为在从LEP到中间代码的翻译中已经处理了代词同样，由于缺乏空间，描述不完整。考虑到前面几节的语法分类，我们有以下重写规则：200C. Bazilio等人/理论计算机科学电子笔记184（2007）189<e2，top，prop>Q<$re-channel-msgs（mid，t））<$re-vars（prop））<$re-runs（mid，top））（mid，bin，bout，assoc，t>，top，prop）（2，顶部，支柱）<，top，prop>Qproctype mid{<$re-locals（aspark））<$re-init（t））（做，顶，支撑）od}Q：：<$ce）→ <$update-vars（ce，prop））<$cm，top，prop）<如果ce{ cm}，top，prop>Qif：：<$ce）→ <$update-vars（ce，prop））<$cm，top，prop）*elsefi在这些规则中，函数mire-channel-msgs定义了给定进程交换的消息通道2.6从通信模型到SMV的与第2.5节类似，我们在这里介绍将通信模型转换为SMV [6]。转换不像转换到Promela那么简单，因为SMV在其基本实现中没有通过通道进行通信的原语Q模块主V AR<$assignre-globals（ e1，e2，top）） ASSIGN<$assign-globals（ e1，e2，top））（1，顶部）（2，顶部）<，top>QMODITORmod mid（ mid，processes，matrix）V AR <$re-locals（ask））<$re-states（ t））ASSIGN？assign-initial-states（ t））？ t，top） F AIRNESSrunning<，cm，top，pos>Qnext（ id）：=case order= pos<$generate-pre-conds（ ce，id，top））：<$ expr）;&esac;<$ce→cm，top，inc（pos））<，cm2，top，pos>Q<$<$ce1）<$ce2）→cm1，top，pos）&<$ce1→cm2，顶部，inc（pos））在转换规则中，函数Bire-main声明网络的实例，并在实例之间传递模块idC. Bazilio等人/理论计算机科学电子笔记184（2007）189201声明一个变量，该变量基于中间代码中相关节点的传入和传出弧存储实例的可能状态之一;assign- initial-states分配变量的初始状态; finally 函数extract- state-transitions将同步和分配命令映射到状态和状态转换。3使用示例在本节中，我们非正式地描述协议DSR的行为此外，我们描述了我们如何对该协议进行建模，假设以及如何在LEP中指定。对于这个模型上的无效属性，我们展示了Spin返回的反例，以及它如何在LEP的抽象级别转换为另一个。3.1DSR规范动态源路由[11]是一种简单有效的移动自组织网络路由协议通过网络发送的每个包通过在访问节点时将节点的标识符添加到其报头来携带其路由。每个节点都保存一个路由缓存，这些路由是由通过该节点发送的包学习的。DSR由两个子协议组成：一个用于查找路由，另一个用于维护路由。当一个节点希望将一个包发送到另一个节点时，它会在本地缓存中搜索到达该目的地的路由。如果搜索成功，包裹将被发送到路由的第一个节点。这在每个节点重复，直到包到达其目的地。如果搜索失败，则激活用于查找路由的子协议。在发生路由错误的情况下，发送路由错误数据包，接收到它的节点更新它们的缓存。这只是DSR的基本版本，还有许多其他的优化方法被提出[11]。3.2DSR建模我们基于以下假设指定协议DSR：（i）我们假设所有希望通信的节点都愿意完全参与协议;(ii)节点不支持干扰（例如，主机同时接收两个不同的消息，这可能导致消息的丢失）;（iii）自组织网络内的节点可以在没有通知的情况下随时移动;（iv）节点是可区分的。在图4中，我们可以看到LEP中手动DSR规范的一部分由于篇幅有限，我们不提供整个协议的详细说明。例如，我们不包括路由的缓存。相反，每个移动主机在需要发送消息时都必须重新计算路由在这里，我们描述了DSR规范摘录中使用的LEP的一些语法细节（图4），这些细节之前没有讨论过。这个规范的语义将在下一段中讨论。由于在拓扑的定义中使用了参数dynamic，因此主机的移动是隐式和自动的。202C. Bazilio等人/理论计算机科学电子笔记184（2007）1891拓扑是任意的（7）无向动态; 2模块跳3456789101112131415161718192021222324252627282930313233(seq int count = 0; intcount =0;真实->packet#1.clean; packet#1.first = this; packet#1.last = anyother（this）; order = { order，order+1 }; packet#2 = order;邻居们！int count（count）;这个吗rr（packet）->如果这== packet#1.last，则packet#1.add（this）;packet#1.previous！unique（）;其他如果没有（packet#1.contains（this）），则packet#1.add（this）;neighbors！intcount（count）;endif结束这个？单播（数据包）->如果这== packet#1.first，则packet#1.next！String（String）;其他packet#1.previous！unique（）;结束这个？数据包->如果this> packet#1.last，则如果neighbors.contains（packet#1.next），则packet#1.next！String（String）;其他发送者！packet_error（packet）;packet.remove34端模块见图4。 LEP中DSR规范摘录matic生成的。在局部声明（第3行）中使用的符号'#'是LEP的类型构造函数，它聚合其他类型以创建一个组合类型。除了基本类型int和bool之外，类型还可以是值序列（seq）或值集。对于这些集合中的每一个，我们都有一组普通的函数来处理它们。完整列表见[1]。在第5-6行中，移动主机选择用于非确定性通信的伙伴。 在规范中，’#’在第6行中，符号（{}）定义为非决定性的选择。最后，在第33行中，未指定对接收分组错误消息的处理。其他命令的工作原理如前所述（第2.2节）。在语义上，在拓扑结构的描述中使用参数dynamic的原因是移动主机可以在任何时间以任何速度移动而不需要通知。也就是说，该等变动独立于规格。所以，我们决定不显式地这样做。移动主机的初始行为是不确定的，因为在DSR协议中，主机可以随时发送消息。变量order用于标识路由请求，以避免重复响应。由于LEP仍然不处理实时问题，我们通过对变量order值的非确定性选择（第6行）对DSR的重传进行建模，这是由对请求的延迟响应超时引起的。如果我们增加这个变量，这意味着C. Bazilio等人/理论计算机科学电子笔记184（2007）189203新的请求。否则，这意味着重新传输。第7行和第15行的sending命令在线路26中，移动主机在接收到要发送的分组之后，验证它是否仍然与分组中的下一个移动主机连接。如果没有连接，则会向该数据包的发送方发送错误消息（数据包错误）。其他转换按预期工作。关于DSR，我们可能有以下属性：财产结果<> p！rr（q）和[]（q！单播（无）和q！rr（无））真[](p！rr）→<>（p！）真[]（没有！数据包错误）假[]（没有！单播（p）U p！）假在该架构向Promela的转换中，通过对节点之间的连接矩阵进行非确定性更改来模拟节点这是可能的，因为移动反映的是可达性而不是物理位置的变化 由于这些更改，属性[]（无！数据包错误）为假。属性（[]（无！单播（p）U p！显然，这是一个错误的公式顺序。Spin中关于模型的属性考虑指定中的全局变量。然后，在转换阶段必须生成许多变量，以便规范和验证上面列出的属性。它强调了手动使用不像Promela那样抽象的特定语言 关于反例，属性的反例[]（无！单播（p）U p！Spin在验证转换为Promela的LEP规范后返回的结果（见图5）。图五.属性[]的反例（无！单播（p）U p！在XSpin中我们的目标是在LEP的抽象层次上获得属性[]的反例（无！单播（p）U p！下面是一个例子：204C. Bazilio等人/理论计算机科学电子笔记184（2007）1891！单播（p）p！Comm该体系结构返回的一个反例是一个动作序列一个2英尺... 其中每个aj是发送/接收命令，其发送者/接收者（actors）必须出现在要验证的属性中，1是反例的起始动作，意味着在它之前没有相关的动作被执行，k是结束动作，意味着在它之后没有动作可以被执行。除了属性的保留字（none，everyone，any（k））之外的任何标识符都是反例中的变量。此外，与属性中一样，具有相同名称的变量将考虑相同的参与者或消息。例如，在反例中，some1（some1是一个生成的变量，它与属性中没有出现的参与者有关）向参与者p发送一条单播消息，经过一些步骤后，它发送一条消息“p”，这与公式[]none！单播（p）Up！Comm.虽然图5中的反例并不难理解，因为它只包含3个参与者和7条交换的消息，但如果我们再增加2个参与者，那么交换的消息数量将增加到37条。无论初始配置如何不同，架构返回的反例在两种情况下都是相同的。与MSC（Message SequenceChart）中的反例相比，LEP层次的反例可以看作是一种简化，它只包含与所分析的性质直接相关的元素。为了提供信息，用于将所选择的模型检查器的反例翻译该变量在LEP规范的关键点更新：在每个模块的开始;在一组转换的开始;在转换动作的开始，即在满足的然后，当在Promela该架构返回的反例是通过以下步骤产生的：（1）生成要被具体化的p r o p r om e l a的n e negationnp r oP romela;（2）当p r op romel a被满足时，对用于该数据的counter-eamp le进行具体化。此时，我们有了模拟命令和标记（与LEP相关）;(3)给定Promela上的标记和命令，我们在原始规范中查找相关的LEP命令;（4）如果相关命令的执行取决于LEP中的先决条件，则先决条件的代理也必须在反
我的内容管理
展开
