Characterizing feedback signal drop patterns in formal verification of networked control systems

In order to obtain resource efficient implementations of control loops on embedded platforms, recently there has been a renewed interest in studying stability and various other quality-of-control (QoC) metrics in the presence of control message drops. Towards this, different methods have been proposed to quantify the impact of message drops on stability and control performance. In this paper we will survey these techniques and clarify the relationship between them. Given a drop pattern that satisfies stability and specified QoC constraints, it is important to check whether an implementation platform satisfies this pattern. In other words, whether the control loop in question may be implemented on this platform. Given an architecture, we will also show how certain notions of expressing drop patterns are easier to verify compared to others.