A SAT-Based Analysis of a Calculus for Wireless Sensor Networks

Xi Wu, Hanne Riis Nielson, Huibiao Zhu

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

In viewing the common unreliability problem in wireless communications, the CWQ calculus (a Calculus for Wireless sensor networks from Quality perspective) was recently proposed for modeling and reasoning about WSNs(Wireless Sensor Networks) and their applications from a quality perspective. The CWQ calculus ensures that sensor nodes, even though in an unreliable communication network, can behave in a reasonable manner. Nevertheless, in CWQ calculus, the topological structure is considered at the network level and it is tightly coupled with the processes and other configurations, this may limit its flexibility. In this paper, to make the CWQ calculus more flexible to be able to model and reason about networks of different topological structures, we extend it to be a parametric framework. In the parametric framework, we extract the topological structure of a network and make it to be a configuration such that all topological structure-changes can be captured by this framework. Moreover, in this paper we also develop a SAT-based analysis of the-extended calculus to avoid reaching error configurations due to unreliable communications in WSNs and use the SAT-solver Z3 to check the vulnerability of the whole network. Finally, we give a real-world case study with the scenario of refueling a car to demonstrate the applicability of the extended calculus and the SAT-based analysis.
Original languageEnglish
Title of host publicationProceedings of the 2015 International Symposium on Theoretical Aspects of Software Engineering (TASE 2015)
PublisherIEEE
Publication date2015
Pages23-30
ISBN (Print)978-1-4673-7612-9
DOIs
Publication statusPublished - 2015
Event9th International Symposium on Theoretical Aspects of Software Engineering (TASE 2015) - Nanjing, China
Duration: 12 Sep 201514 Sep 2015
Conference number: 9
http://tase2015.nuaa.edu.cn/

Conference

Conference9th International Symposium on Theoretical Aspects of Software Engineering (TASE 2015)
Number9
CountryChina
CityNanjing
Period12/09/201514/09/2015
Internet address

Cite this

Wu, X., Nielson, H. R., & Zhu, H. (2015). A SAT-Based Analysis of a Calculus for Wireless Sensor Networks. In Proceedings of the 2015 International Symposium on Theoretical Aspects of Software Engineering (TASE 2015) (pp. 23-30). IEEE. https://doi.org/10.1109/TASE.2015.23