Formal Verification of Weakly-Hard Systems

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.

弱硬实时系统是一种能够以有界方式容忍偶尔的截止期错失的实时系统。与具有硬截止期约束的传统系统相比，它们提供了更大的调度灵活性，从而拓展了系统配置和重配置的设计空间。对于这样一个系统，一个关键问题正是它在仍然满足其功能要求的情况下能够容忍多大程度的截止期错失。在本文中，我们对一类通用的弱硬实时系统的验证问题进行了形式化处理。我们讨论了用于管理可达性分析复杂性的松弛和过近似技术，并基于这些技术开发了算法来验证弱硬实时系统的安全性。实验证明了我们的方法在理解不同弱硬约束的影响以及指导在它们之间进行选择方面的有效性。