SMT based Task and Network level Static Schedule Generation for Time Triggered Networked Systems
In Ethernet based time triggered networks, like TTEthernet, a global communication scheme, for which the schedule synthesis is known to be an NP complete problem, establishes contention free windows for the exchange of messages with guaranteed low latency and minimal jitter. However, in order to achieve end to end determinism at the application level, software tasks running on the end system nodes need to obey a similar execution scheme with tight dependencies towards the network domain. In this paper we address the simultaneous co synthesis of network as well as application schedules for preemptive time triggered tasks communicating in a switched multi speed time triggered network. We use Satisfiability Modulo Theories (SMT) to formulate the scheduling constraints and solve the resulting problem using a state of the art SMT solver. Furthermore, we introduce a novel incremental scheduling approach, based on the demand bound test for asynchronous constrained deadline periodic tasks, which significantly improves scalability for the average case without sacrificing schedulability. We demonstrate the performance of our approach using synthetic network topologies and system configurations.
RTNS