基于质量演算的无线网络形式语义与分析

发布时间：2018-01-26 01:43

  本文关键词： 无线网络 进程演算 程序静态分析理论 形式语义学 程序统一理论　出处：《华东师范大学》2016年博士论文　论文类型：学位论文

【摘要】：无线网络(Wireless Networks)是由一组无线的、可移动的网络节点组合而成的网络体系架构,该网络架构已经被广泛地应用于信息物理融合系统、人工智能、分布式计算、灾害恢复以及军事控制等领域。无线网络与传统的有线网络的区别在于：1)局部广播(Local Broadcast)通信模式：在无线网络中,每个网络节点具有一个消息传输半径,只有在消息发送节点的有效传输范围内的接收节点才能够通过使用与发送节点相同的无线信道接收到发送节点发送的消息；2)节点移动性：无线网络的拓扑结构不再是固定不变的,随着时间的流逝,网络节点会遵循一定的移动模式进行移动,导致整个网络拓扑结构的变化。由于无线网络具有以上两个重要特征,加上网络节点通常暴露于环境中,因此节点之间的通信链路会因为网络特征及环境的影响而具有不可靠性,使得网络节点无法在规定时间内收到预想消息,导致网络资源不可用及系统理想行为的失败,从而大大降低了无线系统的服务质量。特别是对于与安全息息相关的系统而言,不可靠链路可能会导致无线系统的瘫痪,甚至带来一系列多米诺效应。因此,如何刻画无线网络特征、降低网络链路不可靠性带来的影响并提高无线系统服务质量成为重要的研究点。在众多的研究方法中,形式化方法以其精确严密的特征被广泛地应用于各个领域。本文基于无线系统的质量视角,围绕上述研究点,提出无线网络的形式语义与分析方法。论文中提及的“质量视角”是指当分布式无线网络节点处于不可靠通信链路中而导致网络节点预想行为失败时,通过本地设备提供的缺省值机制来确保处于不可靠链路中的节点仍然可以给出一个合理的行为,降低不可靠链路带来的影响,从而提高网络服务质量。论文提出面向无线网络的质量演算,该演算不仅捕捉了无线网络局部广播及节点移动等特性,同时,将质量谓词作为卫兵与广播接收动作相结合,用来刻画当节点接收动作满足一定条件时,节点才能够继续执行后续进程,其与节点缺省值机制共同作用,降低了不可靠链路带来的影响。本文给出质量演算的操作语义及指称语义模型,并对无线网络相关性质进行研究。在静态分析理论的指导下,本文提出基于SAT技术的系统鲁棒性分析方法及基于数据的概率可信性分析方法,分别针对网络通信链路的可靠性以及接收到的数据的概率可信性进行了分析。最后,本文使用研究所得的理论与技术对无线网络在智能楼宇、车联网等实际生活中的案例进行了建模和分析,展示了该研究的实际意义和价值。本文的主要内容与贡献包括：·本文提出了面向无线网络的质量演算CWQ语言与mCWQ语言。CWQ语言引入了带有质量谓词的广播接收动作及网络节点的缺省行为机制,囊括了节点通信的物理因素,如节点位置、通信半径以及通信信道等信息,从进程层和网络层两个层面对无线网络进行了刻画,在捕捉了网络局部广播特性的同时,确保了网络节点面临不可靠链路时仍然可以给出合理的行为,以提高网络的服务质量。为了进一步捕捉无线网络的节点移动性,本文将CWQ语言扩展为带有移动特性的mCWQ语言,引入了时间算子及节点的移动模型,从而更好地刻画了网络拓扑结构的动态变化。·本文研究了无线网络质量演算的语义模型。本文提出了无线网络质量演算的操作语义和指称语义模型。首先给出了CWQ演算的标签转移语义及规约语义两种操作语义形式,并使用和谐定理证明了两个语义形式的一致性。之后,给出了mCWQ演算的参数化标签转移语义,通过语义的变迁规则直观地刻画了网络程序运行的过程及网络节点的运行轨迹；同时给出了mCWQ演算的指称语义模型。基于给定的操作语义及指称语义规则,本文对无线网络的相关性质进行了刻画和研究。·本文分析了无线网络通信链路的可靠性和数据概率可信性。本文提出了基于SAT技术的系统鲁棒性分析方法来避免整个网络由于通信链路的不可靠而到达一个错误状态,并使用SMT求解器Z3进行辅助判断。另外,由于无线网络的系统决策依赖于从各个节点接收到的数据,而网络的通信具有概率特性且接收到的数据具有不同的可信级别,因此,本文提出基于数据的概率可信性分析方法。在该方法中,节点的通信概率与收到的数据的可信级别概率被分开,使得新提出的分析方法具有更好的可扩展性并且更适用于对无线网络应用的分析。
[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.

【学位授予单位】：华东师范大学
【学位级别】：博士
【学位授予年份】：2016
【分类号】：TN92
，

本文编号：1464296