發(fā)布時(shí)間：2018-06-10 08:33

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

【摘要】：無線網(wǎng)絡(luò)己經(jīng)被廣泛運(yùn)用于人們?nèi)粘Ｉ钪械脑S多方面。尤其是在缺少固定基礎(chǔ)設(shè)施的情況下,無線網(wǎng)絡(luò)和無線技術(shù)是合適的通信解決方案,并且正在被廣泛應(yīng)用于實(shí)現(xiàn)信息傳輸?shù)母鞣N通訊場景中。構(gòu)成無線網(wǎng)絡(luò)的基礎(chǔ)物理器件是無線網(wǎng)絡(luò)節(jié)點(diǎn)設(shè)備,這些無線節(jié)點(diǎn)設(shè)備為無線網(wǎng)絡(luò)應(yīng)用的實(shí)現(xiàn)提供了基礎(chǔ)的通信功能。 無線網(wǎng)絡(luò)節(jié)點(diǎn)設(shè)備通常是以無線電波為載體進(jìn)行廣播式的信息發(fā)送,這種無線網(wǎng)絡(luò)的廣播信息發(fā)送模式與傳統(tǒng)的有線以太網(wǎng)絡(luò)中的全局廣播信息發(fā)送模式有所不同。在無線網(wǎng)絡(luò)中,信息數(shù)據(jù)的廣播發(fā)送是局部的,也就是說每個(gè)無線節(jié)點(diǎn)所發(fā)送的信息的傳輸范圍是有限的,只有那些處于節(jié)點(diǎn)傳輸半徑覆蓋范圍內(nèi)的部分接收節(jié)點(diǎn)才能夠接收到所對應(yīng)的節(jié)點(diǎn)廣播發(fā)送的信息。受限于有限的信息傳輸范圍,為了使得不在傳輸范圍內(nèi)的兩個(gè)無線節(jié)點(diǎn)之間能夠?qū)崿F(xiàn)交互,就需要借助其他的中間節(jié)點(diǎn)來建立起一條能夠傳輸信息的路由路徑。路由協(xié)議是實(shí)現(xiàn)無線網(wǎng)絡(luò)中路由路徑的建立和維護(hù)的一種重要機(jī)制,主要是通過各種報(bào)文信息在無線網(wǎng)絡(luò)中的廣播來建立路由路徑。 形式化方法被認(rèn)為是對無線網(wǎng)絡(luò)系統(tǒng)進(jìn)行描述和驗(yàn)證的一種可行并且合適的方式。本文研究面向無線網(wǎng)絡(luò)系統(tǒng)的形式化方法。我們主要研究無線網(wǎng)絡(luò)中與通信交互相關(guān)的無線網(wǎng)絡(luò)特性,包括無線節(jié)點(diǎn)之間的廣播通信交互行為以及無線網(wǎng)絡(luò)中路由協(xié)議建立路由路徑的機(jī)制。 無線網(wǎng)絡(luò)中無線節(jié)點(diǎn)之間的通信實(shí)現(xiàn)了無線網(wǎng)路中最根本的信息交互功能。我們考慮無線廣播通信的各種物理特征,包括了無線節(jié)點(diǎn)的位置、通信范圍、通信頻率等物理因素。針對通信交互等無線節(jié)點(diǎn)底層物理行為的形式化描述和建模通常采用基于通信交互的進(jìn)程代數(shù)演算系統(tǒng)。因此,我們擴(kuò)展無線系統(tǒng)演算引入無線網(wǎng)絡(luò)衛(wèi)兵選擇的概念,基于程序統(tǒng)一理提出了無線演算系統(tǒng)的代數(shù)語義和指稱語義。我們給出了一系列無線系統(tǒng)演算的代數(shù)規(guī)則,研究從代數(shù)語義計(jì)算推導(dǎo)出操作語義的方法。 無線網(wǎng)絡(luò)中的路由協(xié)議借助無線節(jié)點(diǎn)之間的通信交互實(shí)現(xiàn)了無線網(wǎng)絡(luò)中的全局信息交互。針對無線網(wǎng)絡(luò)中路由協(xié)議在路由建立和維護(hù)路由路徑時(shí)的特點(diǎn),我們主要考慮路由協(xié)議實(shí)現(xiàn)路由時(shí)的各種路由信息數(shù)據(jù)的處理機(jī)制。因此我們采用形式化描述語言對無線網(wǎng)絡(luò)AODV路由協(xié)議進(jìn)行形式化建模、分析和驗(yàn)證工作并且將底層的無線節(jié)點(diǎn)的通信交互行為抽象為針對變量的賦值效果。通過使用這種在更高層次的抽象描述方式,我們能夠更直接地分析無線網(wǎng)絡(luò)路由協(xié)議的本質(zhì)特性。 本文的主要貢獻(xiàn)包括： ·我們提出了無線系統(tǒng)演算的代數(shù)語義,給出了一組用于描述無線系統(tǒng)演算并行組合線性展開的代數(shù)規(guī)則,并且定義了無線網(wǎng)絡(luò)系統(tǒng)的規(guī)范型。借助無線網(wǎng)絡(luò)系統(tǒng)的規(guī)范型,我們給出了從代數(shù)語義計(jì)算生成操作語義的方法,并且證明了代數(shù)語義和操作語義的一致性,從代數(shù)語義的角度保證了操作語義的正確性和完備性。我們使用重寫邏輯工具M(jìn)aude實(shí)現(xiàn)了從代數(shù)語義自動(dòng)計(jì)算操作語義的過程。我們提出了無線系統(tǒng)演算的指稱語義,引入了無線網(wǎng)絡(luò)執(zhí)行狀態(tài)和執(zhí)行軌跡的概念用來描述無線網(wǎng)絡(luò)的行為�；谥阜Q語義模型,我們證明了無線網(wǎng)絡(luò)系統(tǒng)的代數(shù)性質(zhì)。 ·我們使用形式化建模語言Z對無線網(wǎng)絡(luò)中使用的AODV路由協(xié)議進(jìn)行建模,并且使用基于Rely/Guarantee方法的形式化驗(yàn)證技術(shù)證明了協(xié)議的性質(zhì)。通過形式化建模語言,我們在建模過程中消除了路由協(xié)議相關(guān)文檔中自然語言描述的二義性。我們使用程序變量賦值的效果來描述無線節(jié)點(diǎn)之間的通信交互。我們對使用形式化語言Z構(gòu)建的協(xié)議模型進(jìn)行重寫得到基于共享變量并行程序語言的改進(jìn)協(xié)議模型。以共享變量并行程序所描述的路由協(xié)議形式化模型為基礎(chǔ),我們使用Rely/Guarantee推理規(guī)則證明了路由協(xié)議建立的路由路徑不存在路由環(huán)路等性質(zhì)。
[Abstract]:Wireless networks have been widely used in many aspects of people ' s daily life . Especially in the absence of fixed infrastructure , wireless networks and wireless technologies are suitable communication solutions and are being widely used in various communication scenarios for information transmission . Basic physical devices forming wireless networks are wireless network node devices that provide a basis for wireless network applications .


in that wireless network , the broadcast transmission of the information data is local , that is to say , the transmission range of the information sent by each wireless node is limited .


Formal methods are considered to be a feasible and suitable way to describe and validate the wireless network system . A formal method for wireless network systems is studied . We mainly study the wireless network characteristics related to communication interaction in wireless networks , including broadcast communication interaction between wireless nodes and mechanisms for establishing routing paths in wireless networks .


The communication between wireless nodes in wireless network realizes the most basic information interaction function in wireless network . We consider various physical characteristics of wireless broadcast communication , including physical factors such as location , communication range and communication frequency of wireless node .


The routing protocol in wireless network realizes global information interaction in wireless network by means of communication interaction between wireless nodes . In view of the characteristics of routing protocol in establishing and maintaining routing paths in wireless network , we mainly consider routing protocols to implement various routing information data processing mechanisms . Therefore , formal description language is used to formally model , analyze and validate the AODV routing protocol , and abstract the communication interaction behavior of the underlying wireless node into the assignment effect for the variable . By using this method of abstraction in higher level , we can analyze the nature of the wireless network routing protocol more directly .


The main contributions of this article include :


The algebraic semantics of wireless system calculus are presented , and a set of algebraic rules for describing the parallel combination of wireless systems are presented , and the canonical form of the wireless network system is defined . By means of the canonical form of the wireless network system , we present the semantics of the operation semantics from the algebraic semantics . We propose the semantic of the operation semantics from the algebraic semantics . We propose the concept of the wireless network execution state and the execution trajectory to describe the behavior of the wireless network . Based on the alleged semantic model , we prove the algebraic properties of the wireless network system .


We use formal modeling language Z to model AODV routing protocols used in wireless networks , and demonstrate the nature of protocols by using formal verification techniques based on Rely
【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2014
【分類號】：TN92

【引證文獻(xiàn)】

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

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

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

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

，

本文編號：2002603