Formal verification of weakly-hard systems

Chao Huang, Wenchao Li, Qi Zhu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationHSCC 2019 - Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems
Subtitle of host publicationComputation and Control
PublisherAssociation for Computing Machinery, Inc
Pages197-207
Number of pages11
ISBN (Electronic)9781450362825
DOIs
StatePublished - Apr 16 2019
Event22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019 - Montreal, Canada
Duration: Apr 16 2019Apr 18 2019

Publication series

NameHSCC 2019 - Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control

Conference

Conference22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019
CountryCanada
CityMontreal
Period4/16/194/18/19

Keywords

  • Formal verification
  • Safety
  • Weakly-hard

ASJC Scopus subject areas

  • Computer Science Applications
  • Computer Networks and Communications
  • Control and Systems Engineering
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Formal verification of weakly-hard systems'. Together they form a unique fingerprint.

Cite this