@inproceedings{af4fd3f87a4f4e6e80418612bfb7e05d,
title = "A Proof System for mCWQ",
abstract = "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 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.",
keywords = "Hoare Logic, Node Mobility, Quality, Wireless Sensor Networks, mCWQ Calculus",
author = "Wanling Xie and Xi Wu and Huibiao Zhu and Gang Lu and Ailun Liu",
note = "Publisher Copyright: {\textcopyright} 2017 IEEE.; 41st IEEE Annual Computer Software and Applications Conference, COMPSAC 2017 ; Conference date: 04-07-2017 Through 08-07-2017",
year = "2017",
month = sep,
day = "7",
doi = "10.1109/COMPSAC.2017.32",
language = "英语",
series = "Proceedings - International Computer Software and Applications Conference",
publisher = "IEEE Computer Society",
pages = "45--50",
editor = "Claudio Demartini and Thomas Conte and Motonori Nakamura and Chung-Horng Lung and Zhiyong Zhang and Kamrul Hasan and Sorel Reisman and Ling Liu and William Claycomb and Hiroki Takakura and Ji-Jiang Yang and Edmundo Tovar and Stelvio Cimato and Ahamed, \{Sheikh Iqbal\} and Toyokazu Akiyama",
booktitle = "Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017",
address = "美国",
}