期刊名称：International Journal of Distributed Sensor Networks
印刷版ISSN：1550-1329
电子版ISSN：1550-1477
出版年度：2015
卷号：2015
DOI：10.1155/2015/257157
出版社：Hindawi Publishing Corporation
摘要：Well-designed wireless sensor networks (WSNs) usually provide vital support for collecting, processing, and forwarding the real-time information in mission-critical applications where medium access control (MAC) protocols determine the channel access control capabilities and the energy consumption properties of these networks. This paper models the MAC protocol of CSMA/CA using timed automata on the message communication and the energy harvesting and analyzes the protocol through model checking of the major CTL properties. The modeling and analysis of CSMA/CA protocol with the comparative experiments give some performance results and also reveal that timing error may cause deadlock, and the accessibility is satisfied if no deadlock exists.
