Formal Specification and Verification of Self-Configuring P2P Networking: A Case Study in Mobile Environments

 In mobile environments (MEs) such as vehicular ad hoc networks (VANETs), mobile ad hoc networks (MANETs), wireless sensor networks (WSNs), and so on, formal specification of self-configuring P2P networking (SPN) emerges as a need for programming, and verifying such mobile networks. Moreover, well-specified SPN in MEs becomes a requirement of developing middleware for the mobile networks. The chapter is a reference material for readers who already have a basic understanding of the MEs for their applications and are now ready to know how to specify and verify formally aspect-oriented self-configuring P2P networking (ASPN) in MEs using categorical language, assured that their computing needs are handled correctly and efficiently. ASPN in MEs is presented in a straightforward fashion by discussing in detail the necessary components and briefly touching on the more advanced components. Several explanatory notes and examples are represented throughout the chapter as a moderation of the formal descriptions. Significant properties of ASPN in MEs, which emerge from the specification, create the firm criteria for verification.