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

Phan Cong-Vinh

Formal and Practical Aspects of Autonomic Computing and Networking: Specification, Development, and Verification. IGI Global, 2012. 170-188. Web. 1 Jul. 2015. doi:10.4018/978-1-60960-845-3.ch007

Book’s link


 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.