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.
Signal stability-based adaptive routing (SSA) for ad hoc mobile networks