WCET-aware reachability for verified simplex design: work-in-progress

Publikationstyp
Conference Paper
Date Issued
2021-09-30
Sprache
English
Author(s)
Lübke, Ole  orcid-logo
Schupp, Sibylle  
Institut
Softwaresysteme E-16  
TORE-URI
http://hdl.handle.net/11420/10710
Start Page
27
End Page
28
Citation
ACM SIGBED International Conference on Embedded Software (EMSOFT 2021)
Contribution to Conference
21st ACM SIGBED International Conference on Embedded Software, EMSOFT 2021  
Publisher DOI
10.1145/3477244.3477613
Scopus ID
2-s2.0-85117436997
Previous online reachability algorithms for hybrid automata reduced conservatism in verified Simplex controller architectures, but were restricted to the imprecise real-time paradigm, i.e., their precision increases over time. Yet, many safety-critical cyber-physical systems are hard real-time systems, requiring an upper bound on the worst-case execution time (WCET) of each task to be known. We show that the iteration bound of the reachability loop can be parameterized by a single factor which determines the precision. Consequently, an algorithm could select a fixed precision depending on the time left until its deadline. In this paper we present such a WCET-aware reachability algorithm, based on an existing algorithm for imprecise real-time. Its smallest WCET bound on an Infineon XMC4500 microprocessor is 32.861 milliseconds.
Subjects
online reachability
simplex
WCET