基于Hoare Logic的无线网络推理系统

发布时间：2018-05-18 13:44

本文选题：无线网络 + 无线系统演算　；参考：《华东师范大学》2017年硕士论文

【摘要】：随着无线网络技术的飞速发展,无线网络产品被应用于人们生活的各个领域。同时,对于无线网络的正确性与安全性的要求也与日俱增。无线网络的形式化验证是重要的验证方式之一,也是时下的研究热点。无线网络形式化验证的理论研究主要采用无线网络语义来刻画网络中节点间通信传输和行为模式的特性。其中,关于无线系统演算(Calculus of Wireless System,CWS)的语义研究国际上已经有了一定的理论研究基础。然而,在公理验证系统领域,当前还没有对该无线系统演算的研究。本文将Hoare Logic公理系统应用于无线网络系统的验证,提出了适用于无线网络系统特性的无线网络推理系统,从而完善了现有无线系统演算的形式化语义模型,并为无线网络系统的自动定理证明机器实现提供理论基础。本文在无线系统演算的操作语义基础上,给出了基于公理系统的基本通信规则。接着,为了验证复杂的分布式无线网络,对并发情况进行了分组归类,提出了并发组合规则和辅助规则,从而完整地给出无线系统演算的推理系统。利用该推理系统能很好地描述无线网络中节点通信间本地广播、同步并发等特性以及通信行为中的冲突情况,从而对无线网络系统中的协议进行建模验证。该推理系统不但为无线网络系统验证方法提供了新的思路,而且也为后续无线系统演算的形式化语义连接理论的研究奠定了理论基础。此外,本文对推理系统中的推理规则进行了逐条证明,完整地证明了本推理系统的可靠性。最后,为了更好地说明本推理系统的表达能力和应用场景,本文分别挑选了无线网络中具有代表性的MAC层的停等协议和网络层的DSR路由协议,对这两种协议进行了形式化地分析建模和性质验证。
[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.
【学位授予单位】：华东师范大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：TN92

【相似文献】