Automata-theoretic modeling of fixed-priority non-preemptive scheduling for formal timing verification

The design process of safety-critical systems requires formal analysis methods to ensure their correct functionality without over-sized safety margins and extensive testing. For architectures with state-based events or scheduling, such as load-dependent frequency scaling, model checking has emerged as a promising tool. It formally verifies timing behavior of realtime systems with minimal over-approximation of the worst case delays. In this context, Event Count Automata (ECAs) have become a valuable modeling approach because they are specifically designed to handle typical arrival patterns and integrate well with analytic techniques. In this work, we propose an extension of the ECA framework´s semantics and use it in a Fixed-Priority Non-preemptive Scheduling (FPNS) model that correctly abstracts the intra-slot behavior in the slotted-time model of the ECA. This is challenging because straightforward implementations cannot capture the full behavior of event-triggered scheduling with such a time model that the ECA shares with most model checking based methods. In a case study, we obtain bounds via model checking a basic model and then our proposed model. We compare these bounds with a SystemC simulation. This shows that the bounds from the basic model are too optimistic - and exceeded in practice - because it does not capture the full behavior, while the bounds from the proposed extended model are both safe and reasonably tight.