Petri net based research of home automation communication protocol

The popularity of home automation has been increasing greatly in recent years. However, during the designation of communication protocol (especially for asymmetric, parallel, distributed, uncertain or randomized protocol model) of home automation, many questions concerned. For instance, is the protocol correct? Is every message eventually delivered and received in the right order? Can two messages with the same alternating bit value be confused? In this paper we adopt Petri net to describe and analyze the protocol of home automation. Through the analysis of dynamic properties (such as reachability, boundedness, coverability and liveness) and invariants on the base of P/T_system modeling and its reachable marking graph, we verified the correctness of the communication protocol and finally optimized the protocol in practice.