Formal Semantics & Analysis On Wireless Networks From Quality Perspective

A wireless network is composed of a group of wireless mobile devices (laptops, PDAs, sensors, etc.), and does not have a fixed network infrastructure. Wireless networks have been widely used in a variety of domains, ranging from Cyber Physical Systems, to ambient intelligence, to distributed computing, to disaster recovery and to military operations. Wireless networks, compared with wired networks, have two important and unique features:1) Local broadcast communication mechanism:In wireless systems, each node has a transmission radius and only the nodes within the transmission area of the sending node can receive the message via a broadcast channel; 2) Node mobility:Instead of a fixed and static network topology structure, nodes in the networks will move following some mobility patterns, leading to the changing of the topology structure.Due to the deployment constraints and features mentioned above, unreliable communications are common in wireless networks; this may lead to an absence of the expected data and an unavailability of network resources, cause the ideal behavior of wireless nodes fail, and decrease the quality of service provided by a wireless system. Unreliable communication may lead to the paralysis of the entire system with a domino effect, especially for safety-critical systems. Motivated by this, how to describe these features, how to reduce the domino effect and how to increase the quality of the service become a significant issue.Among the various research approaches, formal method is widely used in differ-ent fields with its precise characteristics. This thesis proposes formal semantics and analysis on wireless networks from the quality perspective to capture its essential features, such as local broadcast and node mobility. Here, "quality perspective" means that in order to reduce the effect of unreliability of links and increase the quality of service for wireless systems, a default value is provided to wireless nodes from a local device to ensure that the nodes can always behave in a reasonable manner even when they are in unreliable communications and their ideal behaviors fail. The process calculi provided in this thesis not only capture the features of local broadcast and mobility, but also combine the quality predicate as a guard together with default behaviors to ensure a reasonable manner for nodes. Moreover, we inves-tigate the operational semantics and denotational semantics of the process calculi and study the features of networks based on these semantics rules. Furthermore, a SAT-based robustness analysis of the wireless system and a data-driven probabilistic trust analysis are proposed to analyze the reliability of the communication links and the trust level of the input data. We also apply our proposed approach on real-world applications of wireless networks to illustrate its applicability.The main contribution of this paper includes:· We propose the process calculi CWQ and mCWQ for wireless networks from the quality perspective. CWQ calculus specifies a network through both the process level and the network level, combining the quality predicate together with the broadcast receiving actions and giving the default behaviors of nodes in the network. It does not only capture the local broadcast feature, but also ensure the nodes behave in a reasonable manner to increase the quality of service. Moreover, we extend the CWQ calculus into mCWQ calculus, taking the time and mobility models into consideration, to capture the node mobility and describe the change of the topology structure.· We investigate the formal semantic models for the process calculi. We give the reduction semantics and labeled transition semantics for CWQ calculus and prove the correspondence between these two semantics. Moreover, we also give the parametric labeled transition semantics and denotational semantics for the mCWQ calculus. Based on these semantics rules, we can study the properties of wireless networks.· We analyze the reliability of the communication links and the probabilistic trust of the data in the wireless networks. Based on a parametric framework, we investigate a SAT-based analysis approach to avoid the whole network going into an error configuration due to the unreliable communications and use SMT solver Z3 to check it. Furthermore, the decision of the whole network depends on the data received from each receiver. Due to data from different channels have different trust level and different probabilities to be received, thus, we propose a data-driven probabilistic trust analysis for the network to decouple the probability of receiving the data and the probability of the trust level of the data, which makes the new approach more flexible and more suitable for reasoning about the applications of wireless networks.