Abstract
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. Meeting these challenges of mobile networks requires a fundamental approach to the facets of SPN in MEs not tackled before. To this end, taking advantage of the categorical structures we establish, in this chapter, a firm formal basis for specifying P2P, self-configuration, aspect-orientation, and aspect-oriented self-configuring P2P networking (ASPN) in MEs. All of these are to support a mechanism of verification for ASPN in MEs.
TopPreliminaries
In this section, we recall some concepts from the category theory (Asperti & Longo, 1991 ; Bergman, 1998 ; Adamek, Herrlich, & Strecker, 2009 ; Levine, 1998 ; Lawvere & Schanuel, 1997) used in this chapter.
Key Terms in this Chapter
Middleware: Computer software that connects software components or applications.
P2P Networking: Any distributed networking structure composed of participants (so-called peers) that make a portion of their resources (such as processing power, disk storage or network bandwidth) directly available to other network participants, without the need for central coordination instances (such as servers or stable hosts)
Formal Specification: A mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not (necessarily) how the system should do it.
Self-Configuration: A process by which computer systems or networks automatically adapt their own configuration of components without human direct intervention. Self-configuration technologies are expected to permeate among the next generation of computer systems or networks
Formal Verification: An act of proving or disproving, using mathematically-based techniques, the correctness of intended algorithms underlying a system with respect to a certain formal specification or property.
Aspect-Orientation: A software development focuses on the identification, specification and representation of crosscutting concerns and their modularization into separate functional units as well as their automated composition into a working system.
Mobile Computing: A comprehensive term describing ability of systems to use information processing technology while moving, as opposed to portable computers, which are only practical for use while deployed in a stationary configuration.
Formal Methods: A particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems