Reasoning System For Calculus Of Wireless System Based On Hoare Logic

With the rapid development of wireless network technology,wireless network products are widely used in our daily life.Meanwhile,the requirements of the wireless network security are seriously increasing.While the formal verification method of wireless network is one of the significant methods,it is also a hot research topic.The theoretical study of formal verification mainly applies wireless network semantics to describe the properties of transmission and behavior patterns.Among them,semantic research on the calculus of wireless system(CWS)has a certain international theoretical basis.However,there is no research on CWS in the field of axiomatic verification system.Thus,we first try to apply the Hoare Logic to the wireless system verification and propose a wireless network reasoning system,which perfects the formalized semantic model of the existing wireless system calculus and provides the theoretical basis for the implementation of machine proof.This paper first gives the basic communication rules based on the operation semantics of CWS and axiom system.In order to verify the complex distributed wireless network,we then classify the concurrent situations and propose the con-currency rule and auxiliary rules for verification,which completes the reasoning system of CWS.This reasoning system can describe the characteristics of local broadcast,synchronous concurrency,and communication conflicts,so as to model the wireless network protocols.This reasoning system not only provides a new idea for the wireless network system verification method,but also has laid a theoretical basis for the follow-up study of formalized semantic connection theory.In addition,this paper proves the soundness of this reasoning system rigorously,which also ex-plains the correctness of the semantic of the wireless system.Finally,in order to better explain the rich expression ability and application scenarios of the reasoning system,we model the Stop-and-Wait ARQ protocol and the DSR routing protocol as well as verify some properties of these protocols.