A Calculus for Wireless Sensor Networks from Quality Perspective

Due to deployment constraints and communication modalities, unreliable communications are very common in Wireless Sensor Networks (WSNs). In order to ensure that every node can behave in a reasonable manner even though they are in an unreliable communication, we propose CWQ, a process calculus for formal modeling and reasoning about WSNs and their applications from a quality perspective. We combine local broadcast, one of the most important peculiarities of networks, with quality predicate. Default values are given in the case that ideal behaviors of wireless nodes fail because of the unreliable communication, to increase the service quality offered by the system. Moreover, we also give the operational semantics of CWQ in terms of both a Labeled Transition Semantics and a Reduction Semantics, and prove a correspondence result between them. Finally, some examples, and two real-world case studies Smart Home and Smart Grid are used to illustrate the applicability of our calculus.