Formal verification of weakly-hard systems
Chao Huang, Wenchao Li, Qi Xin Zhu · 2019
Weakly-hard systems are real-time systems that can tolerate occasional deadline misses in a bounded manner. Compared with traditional systems with hard deadline constraints, they provide more scheduling flexibility, and thus expand the design space for system configuration and reconfiguration. A key question for such a system is precisely to what degree it can tolerate deadline misses while still meeting its functional requirements. In this paper, we provide a formal treatment to the verification problem of a general class of weakly-hard systems. We discuss relaxation and over-approximation techniques for managing the complexity of reachability analysis, and develop algorithms based upon these for verifying the safety of weakly-hard systems. Experiments demonstrate the effectiveness of our approach in understanding the impact of and guiding the selection among different weakly-hard constraints.