Describing IEEE 802.11 Wireless Mechanisms by Using the π-Calculus and Performance Evaluation Process Algebra

摘要

IEEE 802.11 protocols are formally expressed using the π-calculus process algebra and a performance evaluation process algebra. We first describe the handoff mechanism in wireless LANs, and then the IEEE 802.11 MAC, a medium access control mechanism which is a variant of CSMA/CA. A 4-way handshake mechanism of IEEE 802.11 with fixed network topology is expressed using the π-calculus. The verification process for the specified protocols is briefly described; Mobility Workbench and PEPA Workbench are used as software tools for verification.