Formal Verification of mCWQ Using Extended Hoare Logic

Node mobility, as one of the most important features of Wireless Sensor Networks (WSNs), may affect the reliability of communication links in the networks, leading to abnormalities and decreasing the quality of service provided by WSNs. The mCWQ calculus (i.e., CWQ calculus with mobility) is recently proposed to capture the feature of node mobility and increase the communication quality of WSNs. In this paper, we present a proof system for the mCWQ calculus to prove its correctness. Our specifications and verifications are based on Hoare Logic. In order to describe the timing of observable actions, we extend the assertion language with primitives. And terminating and non-terminating computations both can be described in our proof system. We also give some examples to illustrate the application of our proof system.