Formal methods for stability analysis of networked control systems with IEEE 802.15.4 protocol

Wireless networked control systems (WNCS) with control loops closed over a wireless network are prevailing these days. However, due to uncertainties such as random accessing delays and possible packet drops, the stability analysis for WNCS is a challenging task. Most previous research on the communication network analysis either simply relied on Monte-Carlo simulation or followed the multi-state Markov chain framework. In this paper, we propose a probabilistic model checking methodology for stability analysis in which the communication system is modeled as a probabilistic timed automaton. The stability condition is written in the probabilistic temporal logic which can be checked and the satisfaction of the specification is equivalent to the stability of the WNCS. We then studied the impact of different MAC parameters on the satisfaction of the specification. Furthermore, if the specification is not satisfied initially, we propose a systematic way to design the controller so that the specification can be met. This work presents an attempt and a new angle to the communication and control system co-design problem.