Formal analysis of a calculus for WSNs from quality perspective

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 still behave in a reasonable manner using default values. Nevertheless, the topological structure in CWQ calculus 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, we extend our previous CWQ calculus to be a parametric framework to make it more flexible to be able to model and reason about networks of different topological structures. In the parametric framework, we extract the topological structure of a network and make it to be a configuration so that all topological structure changes can be captured by this framework. Besides, under the guide of program analysis, in this paper, we propose two analysis approaches for the extended CWQ calculus: 1) We develop a SAT-based analysis to check whether default values can always be available, so that some error configurations (e.g., deadlock processes), caused by unreliable communications in WSNs, will not be reached; 2) We also propose a data-driven probabilistic trust analysis to decouple the probability of receiving the expected input data from the probability of the trustworthiness of the data, so that the overall trustworthiness of the system decision is determined by performing a relational analysis to combine these two probability distributions. Finally, we give a real-world case study with the scenario of refueling a car to demonstrate the applicability of the extended calculus and these two analysis approaches on the extended calculus for WSNs.