本文選題：無線網(wǎng)絡(luò) + 無線系統(tǒng)演算　； 參考：《華東師范大學(xué)》2017年碩士論文

【摘要】：隨著無線網(wǎng)絡(luò)技術(shù)的飛速發(fā)展,無線網(wǎng)絡(luò)產(chǎn)品被應(yīng)用于人們生活的各個領(lǐng)域。同時,對于無線網(wǎng)絡(luò)的正確性與安全性的要求也與日俱增。無線網(wǎng)絡(luò)的形式化驗證是重要的驗證方式之一,也是時下的研究熱點。無線網(wǎng)絡(luò)形式化驗證的理論研究主要采用無線網(wǎng)絡(luò)語義來刻畫網(wǎng)絡(luò)中節(jié)點間通信傳輸和行為模式的特性。其中,關(guān)于無線系統(tǒng)演算(Calculus of Wireless System,CWS)的語義研究國際上已經(jīng)有了一定的理論研究基礎(chǔ)。然而,在公理驗證系統(tǒng)領(lǐng)域,當(dāng)前還沒有對該無線系統(tǒng)演算的研究。本文將Hoare Logic公理系統(tǒng)應(yīng)用于無線網(wǎng)絡(luò)系統(tǒng)的驗證,提出了適用于無線網(wǎng)絡(luò)系統(tǒng)特性的無線網(wǎng)絡(luò)推理系統(tǒng),從而完善了現(xiàn)有無線系統(tǒng)演算的形式化語義模型,并為無線網(wǎng)絡(luò)系統(tǒng)的自動定理證明機器實現(xiàn)提供理論基礎(chǔ)。本文在無線系統(tǒng)演算的操作語義基礎(chǔ)上,給出了基于公理系統(tǒng)的基本通信規(guī)則。接著,為了驗證復(fù)雜的分布式無線網(wǎng)絡(luò),對并發(fā)情況進行了分組歸類,提出了并發(fā)組合規(guī)則和輔助規(guī)則,從而完整地給出無線系統(tǒng)演算的推理系統(tǒng)。利用該推理系統(tǒng)能很好地描述無線網(wǎng)絡(luò)中節(jié)點通信間本地廣播、同步并發(fā)等特性以及通信行為中的沖突情況,從而對無線網(wǎng)絡(luò)系統(tǒng)中的協(xié)議進行建模驗證。該推理系統(tǒng)不但為無線網(wǎng)絡(luò)系統(tǒng)驗證方法提供了新的思路,而且也為后續(xù)無線系統(tǒng)演算的形式化語義連接理論的研究奠定了理論基礎(chǔ)。此外,本文對推理系統(tǒng)中的推理規(guī)則進行了逐條證明,完整地證明了本推理系統(tǒng)的可靠性。最后,為了更好地說明本推理系統(tǒng)的表達能力和應(yīng)用場景,本文分別挑選了無線網(wǎng)絡(luò)中具有代表性的MAC層的停等協(xié)議和網(wǎng)絡(luò)層的DSR路由協(xié)議,對這兩種協(xié)議進行了形式化地分析建模和性質(zhì)驗證。
[Abstract]:With the rapid development of wireless network technology, wireless network products are applied in every field of people's life. At the same time, the demand for the correctness and security of wireless network is increasing. Formal verification of wireless networks is one of the most important verification methods, and it is also a hot research topic. The theory of formal verification of wireless networks mainly uses the semantics of wireless networks to describe the characteristics of communication transmission and behavior patterns between nodes in the network. Among them, there has been a theoretical foundation for the semantic research of wireless system calculus (Calculus of Wireless system CWS) in the world. However, in the field of axiomatic verification system, there is no research on this wireless system calculus. In this paper, the Hoare Logic axiom system is applied to the verification of wireless network system, and a wireless network reasoning system suitable for the characteristics of wireless network system is proposed, which improves the formal semantic model of the existing wireless system calculus. It also provides a theoretical basis for the automatic theorem proof of wireless network system. Based on the operation semantics of wireless system calculus, this paper presents the basic communication rules based on axiomatic system. Then, in order to verify the complex distributed wireless network, the concurrent cases are classified into groups, and the concurrent combination rules and auxiliary rules are proposed, thus the reasoning system of wireless system calculus is given. The reasoning system can well describe the characteristics of local broadcast, synchronization and concurrency between nodes in wireless network, and the conflict in communication behavior, thus the protocol in wireless network can be modeled and verified. The reasoning system not only provides a new idea for the verification method of wireless network system, but also lays a theoretical foundation for the research of formal semantic join theory of wireless system calculus. In addition, the reasoning rules in the reasoning system are proved one by one, and the reliability of the reasoning system is proved completely. Finally, in order to better explain the expression ability and application scenario of the reasoning system, this paper selects the representative MAC layer stopping protocol and the network layer DSR routing protocol, respectively. The two protocols are formally analyzed and modeled and their properties verified.
【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2017
【分類號】：TN92

【相似文獻】

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

1 李斌;作為獲取知識工具的推理系統(tǒng)[J];管理科學(xué)文摘;1998年01期

2 李天鐸;依據(jù)事例推理系統(tǒng)是獲得知識的工具[J];管理科學(xué)文摘;1998年11期

3 陳有剛;智能化信息系統(tǒng)中的廣義推理系統(tǒng)[J];計算機研究與發(fā)展;1991年06期

4 李衛(wèi)華，張黔，劉娟，，石自力;歸納法推理系統(tǒng)[J];計算機學(xué)報;1996年03期

5 宋方敏;殷熙堯;;命題演算兩個推理系統(tǒng)的等價性[J];計算機工程與科學(xué);2013年09期

6 嚴雋薇,賀飛鳴,吳啟迪;組織決策支持系統(tǒng)中的知識推理系統(tǒng)[J];組合機床與自動化加工技術(shù);2001年08期

7 侯家利,路羽中;歸納法推理系統(tǒng)模式自動生成的一種實現(xiàn)途徑[J];武漢科技學(xué)院學(xué)報;2004年08期

8 陳建國;潘云鶴;;復(fù)合事例推理的方法研究[J];計算機科學(xué);1998年06期

9 曹忠;李傳中;趙文靜;;平面解析幾何交互推理系統(tǒng)的設(shè)計與實現(xiàn)[J];廣州大學(xué)學(xué)報(自然科學(xué)版);2008年01期

10 馮大政,保錚,焦李成;分布式神經(jīng)網(wǎng)絡(luò)推理原理[J];系統(tǒng)工程與電子技術(shù);1997年09期

相關(guān)會議論文 前4條

1 嚴雋薇;賀飛鳴;吳啟迪;;組織決策支持系統(tǒng)中知識推理系統(tǒng)的實現(xiàn)[A];1998年中國智能自動化學(xué)術(shù)會議論文集（下冊）[C];1998年

2 何方琨;;對偶占優(yōu)推理系統(tǒng)的表示定理的證明[A];第十六屆全國青年通信學(xué)術(shù)會議論文集（上）[C];2011年

3 于津;劉敘華;;基于不確定、不精確知識的推理系統(tǒng)-UKRS[A];1996年中國智能自動化學(xué)術(shù)會議論文集（上冊）[C];1996年

4 倪紅波;種玉珍;吳曉;王海鵬;;CBR在老年人看護系統(tǒng)中的研究與應(yīng)用[A];第四屆和諧人機環(huán)境聯(lián)合學(xué)術(shù)會議論文集[C];2008年

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

1 張琪;基于虛擬現(xiàn)實的化工廠應(yīng)急救援客觀對象推理系統(tǒng)的研究與設(shè)計[D];北京化工大學(xué);2015年

2 張嬌;城市供水管網(wǎng)漏損事故FCR推理系統(tǒng)設(shè)計與實現(xiàn)[D];渤海大學(xué);2016年

3 溫金彪;基于規(guī)則引擎的平面幾何推理系統(tǒng)的設(shè)計與實現(xiàn)[D];電子科技大學(xué);2016年

4 王路遙;基于Hoare Logic的無線網(wǎng)絡(luò)推理系統(tǒng)[D];華東師范大學(xué);2017年

5 吳華池;面向應(yīng)急救援的多預(yù)案演練推理系統(tǒng)的研究與設(shè)計[D];北京化工大學(xué);2014年

6 張菲菲;基于本體的強對流天氣推理系統(tǒng)的研究與實現(xiàn)[D];蘭州大學(xué);2008年

7 閆雙雙;滑輪組混合圖示推理系統(tǒng)[D];天津大學(xué);2014年

8 曾俊t@;文本蘊涵推理系統(tǒng)的研究與實現(xiàn)[D];北京郵電大學(xué);2013年

本文編號：1906054