Formal Verification of mCWQ Using Extended Hoare Logic

被引：2

作者：

Xie, Wanling ^{[1
]}

Zhu, Huibiao ^{[1
]}

Wu, Xi ^{[2
]}

Phan Cong Vinh ^{[3
]}

机构：

[1] East China Normal Univ, Sch Comp Sci & Software Engn, Shanghai Key Lab Trustworthy Comp, Shanghai, Peoples R China

[2] Univ Queensland, Sch ITEE, Brisbane, Qld 4072, Australia

[3] Nguyen Tat Thanh Univ, 300A Nguyen Tat Thanh St,Ward 13,Dist 4, Ho Chi Minh City, Vietnam

来源：

MOBILE NETWORKS & APPLICATIONS | 2019年 / 24卷 / 01期

基金：

中国国家自然科学基金; 新加坡国家研究基金会;

关键词：

Hoare logic; Node mobility; mCWQ calculus; WIRELESS SENSOR NETWORKS; AD-HOC; MOBILITY MODELS; CALCULUS; ALGEBRA;

D O I：

10.1007/s11036-018-1142-8

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：134 / 144

页数：11

共 50 条

[21] Extended Floyd-Hoare Logic over Relational Nominative Data
Nikitchenko, Mykola
Ivanov, Ievgen
Kornilowicz, Artur
Kryvolap, Andrii
INFORMATION AND COMMUNICATION TECHNOLOGIES IN EDUCATION, RESEARCH, AND INDUSTRIAL APPLICATIONS, ICTERI 2017, 2018, 826 : 41 - 64
[22] Formal Verification of Mixed-signal Circuits using Extended PSL
Zhang, Meng
Gao, Deyuan
Fan, Xiaoya
2009 IEEE 8TH INTERNATIONAL CONFERENCE ON ASIC, VOLS 1 AND 2, PROCEEDINGS, 2009, : 1288 - 1293
[23] Reverse Hoare Logic
de Vries, Edsko
Kontavas, Vasileios
SOFTWARE ENGINEERING AND FORMAL METHODS, 2011, 7041 : 155 - 171
[24] Hoare logic in the abstract
Martin, Ursula
Mathiesen, Erik A.
Oliva, Paulo
COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2006, 4207 : 501 - 515
[25] Formal verification logic for hybrid security protocols
Newe, T
Coffey, T
COMPUTER SYSTEMS SCIENCE AND ENGINEERING, 2003, 18 (01): : 17 - 25
[26] Explore your logic with formal verification.
不详
COMPUTER DESIGN, 1996, 35 (07): : 123 - 123
[27] A formal framework for synthesis and verification of logic programs
Avellone, A
Ferrari, M
Fiorentini, C
LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 2001, 2042 : 1 - 17
[28] Formal verification of the RCMP Egress routing logic
Murugesh, P
Tahar, S
ICM'99: ELEVENTH INTERNATIONAL CONFERENCE ON MICROELECTRONICS - PROCEEDINGS, 1999, : 89 - 92
[29] SOUNDNESS OF HOARE LOGIC - AN AUTOMATED PROOF USING LCF
SOKOLOWSKI, S
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1987, 9 (01): : 101 - 120
[30] Towards a formal verification of an authentication protocol using non-monotonic logic
Das, Manik Lal
Narasimhan, V. Lakshmi
PROCEEDINGS OF THE FIFTH INTERNATIONAL CONFERENCE ON INFORMATION TECHNOLOGY: NEW GENERATIONS, 2008, : 545 - 550

← 1 2 3 4 5 →