Formal Methods in Cross Layer Modeling and Optimization of Wireless Networks

The layering principle has been long identified as a way to increase the interoperability and to improve the design of telecommunication protocols, where each layer offers services to adjacent upper layers and requires functionalities from adjacent lower ones. In the past, layering has enabled fast development of interoperable systems, but at the same time limited the performance of the overall architecture, due to the lack of coordination among layers. This issue is particularly relevant for wireless networks, where the very physical nature of the transmission medium introduces several performance limitations for protocols designed for wired networks. To overcome these limitations, a modification of the layering paradigm has been proposed, namely, cross-layer design, or “cross-layering.” Several cross-layering approaches have been proposed in the literature so far. Nevertheless, little formal characterization of the cross-layer interaction among different levels of the protocol stack is available yet. A clear need exists for identifying approaches able to analyze and provide quantitative guidelines for the design of cross-layer solutions, and, more importantly, to decide, in each case, whether cross-layering represents an effective solution or not. This chapter provides a detailed survey of the state-of-the-art and future directions in the usage of formal methods for cross-layer modeling and optimization of wireless networks. The text starts by detailing the principles of layered (ISO/OSI and TCP/IP) protocol stacks as well as the cross-layer paradigm. An overview of the architectures of existing and perspective wireless networks is presented along with an analysis of the potential limitations deriving from the layering approach and detailed description of possible optimization solutions enabled by cross-layer design. Subsequent sections are devoted to the issues of modeling and optimization of wireless networks. The remaining sections cover performance optimization as well as architecture optimization (specifically in terms of signaling). The chapter ends with a summary and outlines about future directions of research on the topic.