跳到主要导航 跳到搜索 跳到主要内容

A Proof System for mCWQ

  • Wanling Xie
  • , Xi Wu
  • , Huibiao Zhu*
  • , Gang Lu
  • , Ailun Liu
  • *此作品的通讯作者
  • East China Normal University
  • University of Queensland

科研成果: 书/报告/会议事项章节 › 会议稿件 › 同行评审

摘要

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.

源语言英语
主期刊名Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017
编辑Sorel Reisman, Sheikh Iqbal Ahamed, Claudio Demartini, Thomas Conte, Ling Liu, William Claycomb, Motonori Nakamura, Edmundo Tovar, Stelvio Cimato, Chung-Horng Lung, Hiroki Takakura, Ji-Jiang Yang, Toyokazu Akiyama, Zhiyong Zhang, Kamrul Hasan
出版商IEEE Computer Society
页45-50
页数6
ISBN(电子版)9781538603673
DOI
出版状态已出版 - 7 9月 2017
活动41st Annual IEEE Computer Software and Applications Conference, COMPSAC 2017 - Torino, 意大利
期限: 4 7月 2017 → 8 7月 2017

丛书

姓名Proceedings - International Computer Software and Applications Conference
卷1
ISSN(印刷版)0730-3157

会议

会议41st Annual IEEE Computer Software and Applications Conference, COMPSAC 2017
国家/地区意大利
市Torino
时期4/07/17 → 8/07/17

学术指纹

探究 'A Proof System for mCWQ' 的科研主题。它们共同构成独一无二的学术指纹。

引用此