本文關(guān)鍵詞： 無(wú)線網(wǎng)絡(luò) 進(jìn)程演算 程序靜態(tài)分析理論 形式語(yǔ)義學(xué) 程序統(tǒng)一理論　出處：《華東師范大學(xué)》2016年博士論文　論文類型：學(xué)位論文

【摘要】：無(wú)線網(wǎng)絡(luò)(Wireless Networks)是由一組無(wú)線的、可移動(dòng)的網(wǎng)絡(luò)節(jié)點(diǎn)組合而成的網(wǎng)絡(luò)體系架構(gòu),該網(wǎng)絡(luò)架構(gòu)已經(jīng)被廣泛地應(yīng)用于信息物理融合系統(tǒng)、人工智能、分布式計(jì)算、災(zāi)害恢復(fù)以及軍事控制等領(lǐng)域。無(wú)線網(wǎng)絡(luò)與傳統(tǒng)的有線網(wǎng)絡(luò)的區(qū)別在于：1)局部廣播(Local Broadcast)通信模式：在無(wú)線網(wǎng)絡(luò)中,每個(gè)網(wǎng)絡(luò)節(jié)點(diǎn)具有一個(gè)消息傳輸半徑,只有在消息發(fā)送節(jié)點(diǎn)的有效傳輸范圍內(nèi)的接收節(jié)點(diǎn)才能夠通過(guò)使用與發(fā)送節(jié)點(diǎn)相同的無(wú)線信道接收到發(fā)送節(jié)點(diǎn)發(fā)送的消息；2)節(jié)點(diǎn)移動(dòng)性：無(wú)線網(wǎng)絡(luò)的拓?fù)浣Y(jié)構(gòu)不再是固定不變的,隨著時(shí)間的流逝,網(wǎng)絡(luò)節(jié)點(diǎn)會(huì)遵循一定的移動(dòng)模式進(jìn)行移動(dòng),導(dǎo)致整個(gè)網(wǎng)絡(luò)拓?fù)浣Y(jié)構(gòu)的變化。由于無(wú)線網(wǎng)絡(luò)具有以上兩個(gè)重要特征,加上網(wǎng)絡(luò)節(jié)點(diǎn)通常暴露于環(huán)境中,因此節(jié)點(diǎn)之間的通信鏈路會(huì)因?yàn)榫W(wǎng)絡(luò)特征及環(huán)境的影響而具有不可靠性,使得網(wǎng)絡(luò)節(jié)點(diǎn)無(wú)法在規(guī)定時(shí)間內(nèi)收到預(yù)想消息,導(dǎo)致網(wǎng)絡(luò)資源不可用及系統(tǒng)理想行為的失敗,從而大大降低了無(wú)線系統(tǒng)的服務(wù)質(zhì)量。特別是對(duì)于與安全息息相關(guān)的系統(tǒng)而言,不可靠鏈路可能會(huì)導(dǎo)致無(wú)線系統(tǒng)的癱瘓,甚至帶來(lái)一系列多米諾效應(yīng)。因此,如何刻畫無(wú)線網(wǎng)絡(luò)特征、降低網(wǎng)絡(luò)鏈路不可靠性帶來(lái)的影響并提高無(wú)線系統(tǒng)服務(wù)質(zhì)量成為重要的研究點(diǎn)。在眾多的研究方法中,形式化方法以其精確嚴(yán)密的特征被廣泛地應(yīng)用于各個(gè)領(lǐng)域。本文基于無(wú)線系統(tǒng)的質(zhì)量視角,圍繞上述研究點(diǎn),提出無(wú)線網(wǎng)絡(luò)的形式語(yǔ)義與分析方法。論文中提及的“質(zhì)量視角”是指當(dāng)分布式無(wú)線網(wǎng)絡(luò)節(jié)點(diǎn)處于不可靠通信鏈路中而導(dǎo)致網(wǎng)絡(luò)節(jié)點(diǎn)預(yù)想行為失敗時(shí),通過(guò)本地設(shè)備提供的缺省值機(jī)制來(lái)確保處于不可靠鏈路中的節(jié)點(diǎn)仍然可以給出一個(gè)合理的行為,降低不可靠鏈路帶來(lái)的影響,從而提高網(wǎng)絡(luò)服務(wù)質(zhì)量。論文提出面向無(wú)線網(wǎng)絡(luò)的質(zhì)量演算,該演算不僅捕捉了無(wú)線網(wǎng)絡(luò)局部廣播及節(jié)點(diǎn)移動(dòng)等特性,同時(shí),將質(zhì)量謂詞作為衛(wèi)兵與廣播接收動(dòng)作相結(jié)合,用來(lái)刻畫當(dāng)節(jié)點(diǎn)接收動(dòng)作滿足一定條件時(shí),節(jié)點(diǎn)才能夠繼續(xù)執(zhí)行后續(xù)進(jìn)程,其與節(jié)點(diǎn)缺省值機(jī)制共同作用,降低了不可靠鏈路帶來(lái)的影響。本文給出質(zhì)量演算的操作語(yǔ)義及指稱語(yǔ)義模型,并對(duì)無(wú)線網(wǎng)絡(luò)相關(guān)性質(zhì)進(jìn)行研究。在靜態(tài)分析理論的指導(dǎo)下,本文提出基于SAT技術(shù)的系統(tǒng)魯棒性分析方法及基于數(shù)據(jù)的概率可信性分析方法,分別針對(duì)網(wǎng)絡(luò)通信鏈路的可靠性以及接收到的數(shù)據(jù)的概率可信性進(jìn)行了分析。最后,本文使用研究所得的理論與技術(shù)對(duì)無(wú)線網(wǎng)絡(luò)在智能樓宇、車聯(lián)網(wǎng)等實(shí)際生活中的案例進(jìn)行了建模和分析,展示了該研究的實(shí)際意義和價(jià)值。本文的主要內(nèi)容與貢獻(xiàn)包括：·本文提出了面向無(wú)線網(wǎng)絡(luò)的質(zhì)量演算CWQ語(yǔ)言與mCWQ語(yǔ)言。CWQ語(yǔ)言引入了帶有質(zhì)量謂詞的廣播接收動(dòng)作及網(wǎng)絡(luò)節(jié)點(diǎn)的缺省行為機(jī)制,囊括了節(jié)點(diǎn)通信的物理因素,如節(jié)點(diǎn)位置、通信半徑以及通信信道等信息,從進(jìn)程層和網(wǎng)絡(luò)層兩個(gè)層面對(duì)無(wú)線網(wǎng)絡(luò)進(jìn)行了刻畫,在捕捉了網(wǎng)絡(luò)局部廣播特性的同時(shí),確保了網(wǎng)絡(luò)節(jié)點(diǎn)面臨不可靠鏈路時(shí)仍然可以給出合理的行為,以提高網(wǎng)絡(luò)的服務(wù)質(zhì)量。為了進(jìn)一步捕捉無(wú)線網(wǎng)絡(luò)的節(jié)點(diǎn)移動(dòng)性,本文將CWQ語(yǔ)言擴(kuò)展為帶有移動(dòng)特性的mCWQ語(yǔ)言,引入了時(shí)間算子及節(jié)點(diǎn)的移動(dòng)模型,從而更好地刻畫了網(wǎng)絡(luò)拓?fù)浣Y(jié)構(gòu)的動(dòng)態(tài)變化�！け疚难芯苛藷o(wú)線網(wǎng)絡(luò)質(zhì)量演算的語(yǔ)義模型。本文提出了無(wú)線網(wǎng)絡(luò)質(zhì)量演算的操作語(yǔ)義和指稱語(yǔ)義模型。首先給出了CWQ演算的標(biāo)簽轉(zhuǎn)移語(yǔ)義及規(guī)約語(yǔ)義兩種操作語(yǔ)義形式,并使用和諧定理證明了兩個(gè)語(yǔ)義形式的一致性。之后,給出了mCWQ演算的參數(shù)化標(biāo)簽轉(zhuǎn)移語(yǔ)義,通過(guò)語(yǔ)義的變遷規(guī)則直觀地刻畫了網(wǎng)絡(luò)程序運(yùn)行的過(guò)程及網(wǎng)絡(luò)節(jié)點(diǎn)的運(yùn)行軌跡；同時(shí)給出了mCWQ演算的指稱語(yǔ)義模型�；诮o定的操作語(yǔ)義及指稱語(yǔ)義規(guī)則,本文對(duì)無(wú)線網(wǎng)絡(luò)的相關(guān)性質(zhì)進(jìn)行了刻畫和研究�！け疚姆治隽藷o(wú)線網(wǎng)絡(luò)通信鏈路的可靠性和數(shù)據(jù)概率可信性。本文提出了基于SAT技術(shù)的系統(tǒng)魯棒性分析方法來(lái)避免整個(gè)網(wǎng)絡(luò)由于通信鏈路的不可靠而到達(dá)一個(gè)錯(cuò)誤狀態(tài),并使用SMT求解器Z3進(jìn)行輔助判斷。另外,由于無(wú)線網(wǎng)絡(luò)的系統(tǒng)決策依賴于從各個(gè)節(jié)點(diǎn)接收到的數(shù)據(jù),而網(wǎng)絡(luò)的通信具有概率特性且接收到的數(shù)據(jù)具有不同的可信級(jí)別,因此,本文提出基于數(shù)據(jù)的概率可信性分析方法。在該方法中,節(jié)點(diǎn)的通信概率與收到的數(shù)據(jù)的可信級(jí)別概率被分開,使得新提出的分析方法具有更好的可擴(kuò)展性并且更適用于對(duì)無(wú)線網(wǎng)絡(luò)應(yīng)用的分析。
[Abstract]:The wireless network (Wireless Networks) is a group of wireless network architecture, the combination of mobile network nodes and the network architecture has been widely used in physical information fusion system, artificial intelligence, distributed computing, disaster recovery, military control and other fields. The difference between the wireless network and traditional wired network is: 1) local radio (Local Broadcast): the mode of communication in a wireless network, each network node has a message transmission radius, only in the effective transmission range of message sending nodes within the receiving node to wireless channel by using the same and the sending node receives the sending node message; 2) node mobility: the topology of the wireless network is no longer fixed, with the passage of time, the mobile network node will follow a certain mode of movement, causing the entire network extension On the change of structure. Because the wireless network has more than two important characteristics of network nodes and are usually exposed to the environment, so that the communication links between nodes because of network characteristics and the environment is not reliability, makes the network node cannot receive the desired message within the specified time, leading to the ideal behavior and cyber source is not available the failure of the system, thereby greatly reducing the wireless quality of service system. Especially for the security of the system, unreliable links may lead to paralysis of the wireless system, and even bring a series of the Domino effect. Therefore, how to describe the characteristics of wireless network, reduce the impact of network link reliability and improve the service quality of the wireless system become an important research point. In many methods, formal methods for its precise characteristics are widely used in various A field. In this paper, the perspective of the quality of wireless system based on the above research, put forward the formal semantics and analysis methods of wireless network. This paper mentioned in the "quality perspective" refers to when the distributed wireless network node is unreliable communication links in which network nodes expected behavior fails, the default provided by local device value mechanism to ensure that in the unreliable node link can still give a reasonable behavior, reduce the effect of unreliable link brings, so as to improve the quality of network service. The quality of calculus for wireless networks, the algorithm not only capture the local broadcasting wireless network and mobile node characteristics, at the same time, the quality of the predicate as guards and broadcast receiving action combination is used to describe when the node receives the action to meet certain conditions, the node can continue to perform the following process with the node The default mechanism of interaction, reduce the influence of unreliable links bring. This paper presents the operational semantics and the denotational semantics of the calculus of quality model, and to study the wireless network related properties. In the static analysis under the guidance of the theory in this paper, and the probability of credible data analysis method based on method of system robustness analysis based on SAT technology. Were used for reliability analysis of network communication link and the received data credibility probability. Finally, the theory and techniques used in this paper to study the wireless network in the intelligent building, car networking and other real life case to carry on the modeling and analysis, the study shows the actual significance and value of the main content of this paper. The contribution includes: This paper presented the wireless network quality of CWQ calculus and mCWQ language.CWQ language is introduced with a wide quality predicate The default behavior and action mechanism of receiving broadcast network nodes, including physical factors such as communication node, node location, communication radius and communication channel information is described. In the face of wireless network from the process layer and the network layer two layer, the characteristics of the network to capture the local broadcast at the same time, to ensure that the network node is still facing can give a reasonable behavior of unreliable links, in order to improve the quality of network service. In order to further capture the mobility of wireless network, this paper will be extended to CWQ language with mobile characteristics of the mCWQ language, introduce the mobile operator and the node model, in order to better characterize the dynamic changes of network topology, this paper. Research on the semantic model of wireless network quality calculus. This paper presents semantic quality of wireless network calculus and denotational semantics model. Firstly, CWQ calculus label Transfer protocol two operation semantics and semantic semantic form, and use the harmonious theorem to prove the consistency of the two semantic form. After the parameters are given the label of mCWQ calculus semantic transfer, through the change rule semantic depicts the running track of network program and network node; and gives reference the semantic model of mCWQ calculus. The operational semantics and the denotational semantics given in this paper based on the rules, related properties of wireless networks are characterized and studied. This paper analyzes the reliability and credibility of the data probability of wireless network communication link is put forward in this paper. The robustness analysis method based on SAT technology to avoid the whole network to a error state due to unreliable communication links, and the auxiliary judgment using the SMT solver Z3. In addition, because the system decision depends on the wireless network from various The data node receives, and network communication has the characteristics and probability of the received data with different trust level, therefore, probabilistic reliability analysis method is presented in this paper based on the data. In this method, the probability of nodes and trust level of communication data received by the probability of being separated from the analysis of the proposed method better scalability and more suitable for the analysis of the application of the wireless network.

【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2016
【分類號(hào)】：TN92
，

本文編號(hào)：1464296