面向无线网络的形式化方法研究

发布时间：2018-06-10 08:33

本文选题：无线系统演算 + 代数规则　；参考：《华东师范大学》2014年博士论文

【摘要】：无线网络己经被广泛运用于人们日常生活中的许多方面。尤其是在缺少固定基础设施的情况下,无线网络和无线技术是合适的通信解决方案,并且正在被广泛应用于实现信息传输的各种通讯场景中。构成无线网络的基础物理器件是无线网络节点设备,这些无线节点设备为无线网络应用的实现提供了基础的通信功能。无线网络节点设备通常是以无线电波为载体进行广播式的信息发送,这种无线网络的广播信息发送模式与传统的有线以太网络中的全局广播信息发送模式有所不同。在无线网络中,信息数据的广播发送是局部的,也就是说每个无线节点所发送的信息的传输范围是有限的,只有那些处于节点传输半径覆盖范围内的部分接收节点才能够接收到所对应的节点广播发送的信息。受限于有限的信息传输范围,为了使得不在传输范围内的两个无线节点之间能够实现交互,就需要借助其他的中间节点来建立起一条能够传输信息的路由路径。路由协议是实现无线网络中路由路径的建立和维护的一种重要机制,主要是通过各种报文信息在无线网络中的广播来建立路由路径。形式化方法被认为是对无线网络系统进行描述和验证的一种可行并且合适的方式。本文研究面向无线网络系统的形式化方法。我们主要研究无线网络中与通信交互相关的无线网络特性,包括无线节点之间的广播通信交互行为以及无线网络中路由协议建立路由路径的机制。无线网络中无线节点之间的通信实现了无线网路中最根本的信息交互功能。我们考虑无线广播通信的各种物理特征,包括了无线节点的位置、通信范围、通信频率等物理因素。针对通信交互等无线节点底层物理行为的形式化描述和建模通常采用基于通信交互的进程代数演算系统。因此,我们扩展无线系统演算引入无线网络卫兵选择的概念,基于程序统一理提出了无线演算系统的代数语义和指称语义。我们给出了一系列无线系统演算的代数规则,研究从代数语义计算推导出操作语义的方法。无线网络中的路由协议借助无线节点之间的通信交互实现了无线网络中的全局信息交互。针对无线网络中路由协议在路由建立和维护路由路径时的特点,我们主要考虑路由协议实现路由时的各种路由信息数据的处理机制。因此我们采用形式化描述语言对无线网络AODV路由协议进行形式化建模、分析和验证工作并且将底层的无线节点的通信交互行为抽象为针对变量的赋值效果。通过使用这种在更高层次的抽象描述方式,我们能够更直接地分析无线网络路由协议的本质特性。本文的主要贡献包括： ·我们提出了无线系统演算的代数语义,给出了一组用于描述无线系统演算并行组合线性展开的代数规则,并且定义了无线网络系统的规范型。借助无线网络系统的规范型,我们给出了从代数语义计算生成操作语义的方法,并且证明了代数语义和操作语义的一致性,从代数语义的角度保证了操作语义的正确性和完备性。我们使用重写逻辑工具Maude实现了从代数语义自动计算操作语义的过程。我们提出了无线系统演算的指称语义,引入了无线网络执行状态和执行轨迹的概念用来描述无线网络的行为。基于指称语义模型,我们证明了无线网络系统的代数性质。 ·我们使用形式化建模语言Z对无线网络中使用的AODV路由协议进行建模,并且使用基于Rely/Guarantee方法的形式化验证技术证明了协议的性质。通过形式化建模语言,我们在建模过程中消除了路由协议相关文档中自然语言描述的二义性。我们使用程序变量赋值的效果来描述无线节点之间的通信交互。我们对使用形式化语言Z构建的协议模型进行重写得到基于共享变量并行程序语言的改进协议模型。以共享变量并行程序所描述的路由协议形式化模型为基础,我们使用Rely/Guarantee推理规则证明了路由协议建立的路由路径不存在路由环路等性质。
[Abstract]:Wireless network has been widely used in many aspects of people's daily life. Especially in the absence of fixed infrastructure, wireless network and wireless technology are suitable communication solutions, and are being widely used in all kinds of communication scenes to realize information transmission. The basic physical devices that constitute the wireless network are not Wireless network node devices, these wireless node devices provide a basic communication function for the realization of wireless network applications.
The wireless network node equipment is usually transmitted by radio wave, which is different from the traditional broadcast information transmission mode in the traditional cable Ethernet network. In the wireless network, the broadcast of information data is local, that is, each wireless node. The transmission range of the message sent is limited, only those receiving nodes within the coverage of the node transmission radius can receive the information sent by the corresponding nodes. Limited to the limited information transmission range, in order to enable the interaction between the two wireless nodes within the transmission range, It is necessary to build a routing path that can transmit information with the help of other intermediate nodes. Routing protocol is an important mechanism for the establishment and maintenance of the path in the wireless network. It is mainly to establish routing path through the broadcast of various message information in the wireless network.
Formal methods are considered as a feasible and appropriate way to describe and verify wireless network systems. In this paper, a formal approach to wireless network systems is studied. We mainly study the characteristics of wireless networks related to communication interaction in wireless networks, including radio communication interaction between nodes and no Routing mechanism is established by routing in a network.
Communication among wireless nodes in wireless networks realizes the most fundamental information interaction in wireless networks. We consider the physical features of radio broadcasting communications, including the physical factors of the location, range and frequency of wireless nodes. Formal description and modeling of the underlying physical behavior of wireless nodes, such as communication interaction, are described. A process algebra calculus system based on communication interaction is usually used. Therefore, we extend the concept of wireless network calculus to introduce wireless network guard selection, and propose algebraic semantics and referential semantics of wireless calculus system based on program unification. We give a series of algebraic rules of wireless system calculus, and study from algebraic Semantic Computing. A method of deriving the operation semantics.
The routing protocols in wireless networks implement the global information interaction in wireless networks with the aid of communication interaction between wireless nodes. We mainly consider the processing mechanism of routing information data processing for routing protocols for routing protocols when routing is established and maintained by routing protocols in wireless networks. Formal description language is used to form the formal modeling, analysis and verification of wireless network AODV routing protocol and to abstract the communication interaction between the underlying wireless nodes as the assignment effect for the variable. By using this kind of higher level abstract description, we can analyze the wireless network routing protocol more directly. The essential characteristics.
The main contributions of this article include:
We present the algebraic semantics of wireless system calculus, give a set of algebraic rules to describe the parallel combined linear expansion of wireless system calculus, and define the norm of the wireless network system. With the help of the standard type of the wireless network system, we give the method of generating the operation semantics from the algebraic semantics, and proves that the method of generating the operation semantics from the algebraic semantics is proved. The consistency of algebraic semantics and operational semantics ensures the correctness and completeness of operational semantics from the perspective of algebraic semantics. We use rewriting logic tool Maude to realize the process of automatic operation semantics from algebraic semantics. We propose the referential semantics of the wireless system calculus, and introduce the execution state and execution of the wireless network. The concept of trace is used to describe the behavior of wireless networks. Based on the denotational semantic model, we prove the algebraic properties of wireless network systems.
We use formal modeling language Z to model the AODV routing protocol used in the wireless network, and use the formal verification technology based on Rely/Guarantee method to prove the nature of the protocol. By formalized modeling language, we eliminate the two sense of the natural language description in the routing protocol related documents in the modeling process. We use the effect of the program variable assignment to describe the communication interaction between the wireless nodes. We rewrite the improved protocol model based on the shared variable parallel program language using the protocol model constructed by the formal language Z. Based on the formal model of the routing protocol described by the shared variable parallel program, we use the R The ely/Guarantee inference rule proves that the routing path established by the routing protocol does not exist such as the routing loop.
【学位授予单位】：华东师范大学
【学位级别】：博士
【学位授予年份】：2014
【分类号】：TN92

【引证文献】