real-time system engineers

Abstract: This paper provides a counterexample of the sufficient schedulability test for self-suspending real-time tasks under EDF-Like scheduling given by Wang et al. in Theorem 11 of IEEE Transactions on Computers, 74(7):2364-2375, 2025. This paper also shows that their necessary condition is unsound.

Abstract: In this paper, we study online paging with delay or deadlines. In online paging with delay, an online algorithm manages a cache of size $k$ and needs to serve incoming requests by adding the requested pages to the cache. In addition, it has the option to delay serving incoming requests at a cost that depends on the delay. We propose a new online algorithm, which combines a threshold rule with first-in, first-out (FIFO) replacement, and show that it is $(2k+2)$-competitive for cache size $k$. This result corrects a previously published claim that the competitive ratio is exactly $2k+1$ regardless of the number of holes (pages outside the cache). However, in the case of one hole, we show that the FIFO rule with a different threshold is indeed $(2k+1)$-competitive, giving a tight result. In the case of deadlines, the same analysis gives a deadline-triggered algorithm that is $(k+1)$-competitive in general and $k$-competitive if there is only one hole. Moreover, we show that the second hole makes paging with deadlines strictly harder than classical paging, where the competitive ratio is independent of the number of holes. For paging with deadlines, we prove a deterministic lower bound of $k+\tfrac12$, already for two holes. We show that, as a consequence, no threshold-triggered algorithm can achieve a competitive ratio less than $2k+\frac32$ in general.

Abstract: Timed automata, which extend finite state automata by introducing clock variables, serve as a popular formalism for specifying and analyzing the timed behaviors of real-time systems. Extracting the timed behaviors of a black-box, safety-critical system is crucial for designing and analyzing its real-time requirements, yet it remains challenging. In this paper, we address this problem by generating a deterministic timed automaton (DTA) consistent with a given set of system behaviors, comprising both positive and negative examples. To this end, we adapt the formalism of simple elementary languages (sEL) and introduce the timed augmented prefix tree acceptor (tAPTA). Our approach proceeds as follows: First, we preprocess samples by translating them into sEL, which discards redundancy and detects conflicts; then, we rewrite the resulting sELs in an incremental form and construct a tAPTA to further simplify the samples; finally, we encode the search for a DTA that accepts the simplified tAPTA as an SMT formula. We evaluate our approach on randomly generated benchmarks and a scheduling case study. The results demonstrate the effectiveness of our simplification method in reducing the size of the encoded SMT formula and the efficiency of our approach in mining a DTA.

Abstract: In this paper, we characterize resilience for a labeled real-time automaton (LRTA). An LRTA is resilient if whenever a faulty event occurs, after sufficiently many events occur, the LRTA returns to normalcy and the occurrence of the faulty event is not leaked. The notion of resilience reflects the ability of an LRTA recovering from a faulty behavior, and hence can model an intelligent agent. We formulate one definition of resilience for an LRTA and give verification algorithms for the definition based on two basic tools --- concurrent composition and observer.