Formal Methods On Wireless Networks

Wireless networks have become prevalent relatively recently in our daily life. Wireless networks and applications are suitable solutions and being deployed in a wide range of communication scenarios, especially in infrastructurcless situations. Wireless devices are the basic components of wireless networks, which provide basic functions of communication and implement applications in wireless networks.Wireless devices communicate with each other by broadcasting messages, which is quite different from the more conventional wired-based broadcast in Ethernet systems. Broadcast in wireless networks is local, i.e., a transmission covers a limited range and only a subset of all the devices in the network can receive the broadcasted message. Due to the limited transmission range of wireless devices, two remote wireless devices cannot communicate with each other directly. In order to transfer messages to a wireless device from a distance of another device, it is necessary to establish a routing path via intermediate devices. Routing protocols are important mechanism for wireless networks to establish and maintain routing paths among wireless devices by broadcasting routing messages.To explore wireless networks, formalisms are proposed as feasible and suitable methods to specify and verify communication features of such systems. The main motivation of this paper is to explore the formalisms on the wireless networks. We focus on communication features of wireless networks including the interactions among wireless devices as well as routing protocols used in wireless networks.The interactions among wireless devices provide the basic communication func-tion in wireless networks. We consider the physical aspects of broadcasting com-munication including location, transmission range and communication frequency. Communication based process algebras are common approaches to formalising the low level interactions behaviours among wireless devices. We extend the Calculus of Wireless Systems by introducing the concept of guarded choice. On the basis of Unifying Theories of Programming, we propose the algebraic semantics and the denotational semantics of the calculus. We present a set of algebraic laws for the cal-culus and investigate the derivation strategy for deriving the operational semantics from the algebraic semantics.Routing protocol of wireless networks transfers information in the network via communication function of wireless devices. According to the features when rout-ing protocol establishes and maintains routes, we focus on the protocol mechanism about the route information. Hence, we use formal specification language to specify, analyse and verify the AODV routing protocol. We abstract the interactions among wireless devices as the effects of assignments on variables. Under this high level ab-straction of communication, we can analyze the essential characteristics of routing protocol in wireless networks directly.The main contribution of this paper includes:●We propose the algebraic semantics of the Calculus of Wireless Systems. A set of parallel expansion laws is provided and the head normal form is pre-sented. Based on the head normal form, the derivation strategy for deriving the operational semantics from the algebraic semantics is defined. The equiv-alence between the derivation strategy and the derived operational semantics is proved, which shows the soundness and the completeness of the operational semantics from the viewpoint of the algebraic semantics. We also mechanized the linking between the algebraic semantics and the operational semantics by using rewriting logic in Maude. We also propose the denotational semantic-s for this calculus by introducing the concepts of execution state and trace to describe the behaviour of wireless networks. Based on the denotational semantics, we prove some algebra laws of wireless networks.●We formalise the AODV routing protocol used in wireless network by for-mal specification language Z and prove properties of this protocol uising Re-ly/Guarantee method. Formal description language is used to reduce the am-biguous in protocol description documents. The interaction among devices is modelled as effects of assignments on variables. We rewrite the model speci-fied by Z into a revised version of model based on shared variable concurrent programs. Based on the revised model specified by shared variable concur-rent program, the loop freedom property and other properties of the routing protocol are verified by using the Rely/Guarantee rules.