TY - GEN
T1 - Formal verification of weakly-hard systems
AU - Huang, Chao
AU - Li, Wenchao
AU - Zhu, Qi
N1 - Funding Information:
We gratefully acknowledge the support from the National Science Foundation awards 1834701, 1834324, 1839511, and 1724341. This work is also funded in part by the DARPA BRASS program under agreement number FA8750-16-C-0043 and NSF grant CCF-1646497.
Publisher Copyright:
© 2019 ACM.
PY - 2019/4/16
Y1 - 2019/4/16
N2 - 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.
AB - 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.
KW - Formal verification
KW - Safety
KW - Weakly-hard
UR - http://www.scopus.com/inward/record.url?scp=85064979149&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85064979149&partnerID=8YFLogxK
U2 - 10.1145/3302504.3311811
DO - 10.1145/3302504.3311811
M3 - Conference contribution
AN - SCOPUS:85064979149
T3 - HSCC 2019 - Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control
SP - 197
EP - 207
BT - HSCC 2019 - Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems
PB - Association for Computing Machinery, Inc
T2 - 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019
Y2 - 16 April 2019 through 18 April 2019
ER -