本文選題：無線系統(tǒng)演算 + 代數(shù)規(guī)則　； 參考：《華東師范大學(xué)》2014年博士論文

【摘要】：無線網(wǎng)絡(luò)己經(jīng)被廣泛運用于人們?nèi)粘Ｉ钪械脑S多方面。尤其是在缺少固定基礎(chǔ)設(shè)施的情況下,無線網(wǎng)絡(luò)和無線技術(shù)是合適的通信解決方案,并且正在被廣泛應(yīng)用于實現(xiàn)信息傳輸?shù)母鞣N通訊場景中。構(gòu)成無線網(wǎng)絡(luò)的基礎(chǔ)物理器件是無線網(wǎng)絡(luò)節(jié)點設(shè)備,這些無線節(jié)點設(shè)備為無線網(wǎng)絡(luò)應(yīng)用的實現(xiàn)提供了基礎(chǔ)的通信功能。 無線網(wǎng)絡(luò)節(jié)點設(shè)備通常是以無線電波為載體進行廣播式的信息發(fā)送,這種無線網(wǎng)絡(luò)的廣播信息發(fā)送模式與傳統(tǒng)的有線以太網(wǎng)絡(luò)中的全局廣播信息發(fā)送模式有所不同。在無線網(wǎng)絡(luò)中,信息數(shù)據(jù)的廣播發(fā)送是局部的,也就是說每個無線節(jié)點所發(fā)送的信息的傳輸范圍是有限的,只有那些處于節(jié)點傳輸半徑覆蓋范圍內(nèi)的部分接收節(jié)點才能夠接收到所對應(yīng)的節(jié)點廣播發(fā)送的信息。受限于有限的信息傳輸范圍,為了使得不在傳輸范圍內(nèi)的兩個無線節(jié)點之間能夠?qū)崿F(xiàn)交互,就需要借助其他的中間節(jié)點來建立起一條能夠傳輸信息的路由路徑。路由協(xié)議是實現(xiàn)無線網(wǎng)絡(luò)中路由路徑的建立和維護的一種重要機制,主要是通過各種報文信息在無線網(wǎng)絡(luò)中的廣播來建立路由路徑。 形式化方法被認(rèn)為是對無線網(wǎng)絡(luò)系統(tǒng)進行描述和驗證的一種可行并且合適的方式。本文研究面向無線網(wǎng)絡(luò)系統(tǒng)的形式化方法。我們主要研究無線網(wǎng)絡(luò)中與通信交互相關(guān)的無線網(wǎng)絡(luò)特性,包括無線節(jié)點之間的廣播通信交互行為以及無線網(wǎng)絡(luò)中路由協(xié)議建立路由路徑的機制。 無線網(wǎng)絡(luò)中無線節(jié)點之間的通信實現(xiàn)了無線網(wǎng)路中最根本的信息交互功能。我們考慮無線廣播通信的各種物理特征,包括了無線節(jié)點的位置、通信范圍、通信頻率等物理因素。針對通信交互等無線節(jié)點底層物理行為的形式化描述和建模通常采用基于通信交互的進程代數(shù)演算系統(tǒng)。因此,我們擴展無線系統(tǒng)演算引入無線網(wǎng)絡(luò)衛(wèi)兵選擇的概念,基于程序統(tǒng)一理提出了無線演算系統(tǒng)的代數(shù)語義和指稱語義。我們給出了一系列無線系統(tǒng)演算的代數(shù)規(guī)則,研究從代數(shù)語義計算推導(dǎo)出操作語義的方法。 無線網(wǎng)絡(luò)中的路由協(xié)議借助無線節(jié)點之間的通信交互實現(xiàn)了無線網(wǎng)絡(luò)中的全局信息交互。針對無線網(wǎng)絡(luò)中路由協(xié)議在路由建立和維護路由路徑時的特點,我們主要考慮路由協(xié)議實現(xiàn)路由時的各種路由信息數(shù)據(jù)的處理機制。因此我們采用形式化描述語言對無線網(wǎng)絡(luò)AODV路由協(xié)議進行形式化建模、分析和驗證工作并且將底層的無線節(jié)點的通信交互行為抽象為針對變量的賦值效果。通過使用這種在更高層次的抽象描述方式,我們能夠更直接地分析無線網(wǎng)絡(luò)路由協(xié)議的本質(zhì)特性。 本文的主要貢獻包括： ·我們提出了無線系統(tǒng)演算的代數(shù)語義,給出了一組用于描述無線系統(tǒng)演算并行組合線性展開的代數(shù)規(guī)則,并且定義了無線網(wǎng)絡(luò)系統(tǒng)的規(guī)范型。借助無線網(wǎng)絡(luò)系統(tǒng)的規(guī)范型,我們給出了從代數(shù)語義計算生成操作語義的方法,并且證明了代數(shù)語義和操作語義的一致性,從代數(shù)語義的角度保證了操作語義的正確性和完備性。我們使用重寫邏輯工具Maude實現(xiàn)了從代數(shù)語義自動計算操作語義的過程。我們提出了無線系統(tǒng)演算的指稱語義,引入了無線網(wǎng)絡(luò)執(zhí)行狀態(tài)和執(zhí)行軌跡的概念用來描述無線網(wǎng)絡(luò)的行為。基于指稱語義模型,我們證明了無線網(wǎng)絡(luò)系統(tǒng)的代數(shù)性質(zhì)。 ·我們使用形式化建模語言Z對無線網(wǎng)絡(luò)中使用的AODV路由協(xié)議進行建模,并且使用基于Rely/Guarantee方法的形式化驗證技術(shù)證明了協(xié)議的性質(zhì)。通過形式化建模語言,我們在建模過程中消除了路由協(xié)議相關(guān)文檔中自然語言描述的二義性。我們使用程序變量賦值的效果來描述無線節(jié)點之間的通信交互。我們對使用形式化語言Z構(gòu)建的協(xié)議模型進行重寫得到基于共享變量并行程序語言的改進協(xié)議模型。以共享變量并行程序所描述的路由協(xié)議形式化模型為基礎(chǔ),我們使用Rely/Guarantee推理規(guī)則證明了路由協(xié)議建立的路由路徑不存在路由環(huán)路等性質(zhì)。
[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.
【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2014
【分類號】：TN92

【引證文獻】

相關(guān)期刊論文 前1條

1 龍勇;;淺談計算機網(wǎng)絡(luò)中無線技術(shù)的應(yīng)用[J];電腦知識與技術(shù);2015年18期

相關(guān)碩士學(xué)位論文 前1條

1 李群;基于ATL的形式化建模與驗證技術(shù)的應(yīng)用研究[D];暨南大學(xué);2016年

，

本文編號：2002602