SMT-based Schedule Synthesis for Deterministic Networks
Date:
Tuesday, March 14, 2017 16:30 - 17:30
Speaker:
Silviu Craciunas (TTTech)
Location:
Computer Science Room (I01.2OG.)
Series:
Mathematics and CS Seminar
Host:
Tom Henzinger
Contact:
BONVENTRE-DARTHE Astrid
Ethernet has evolved to be the standard open communication mechanism for a wide range of application domains originally not bound to strict timing requirements. In the real-time domain, safety-critical timing aspects have been introduced by means of technologies like TTEthernet and Time-Sensitive Networks (TSN). In both technologies communication typically follows an offline and statically configured schedule (the synthesis of which is an NP-complete problem) guaranteeing contention-free frame transmissions. In the context of TTEthernet, we present methods for the simultaneous co-generation of static network and task schedules for distributed systems consisting of preemptive time-triggered tasks which communicate over switched multi-speed time-triggered networks. Furthermore we present an incremental scheduling approach, based on the demand bound test for asynchronous tasks, which significantly improves the scalability of the scheduling problem for the average case. In the context of TSN we identify and analyze key functional parameters affecting the deterministic behaviour of real-time communication under 802.1Qbv and, based on a generalized configuration of these parameters, derive the required constraints for computing offline schedules for critical communication flows. We formulate the scheduling problem for both cases using first-order logic with equality and present alternative methods to find a solution, with or without optimization objectives, based on Optimization Modulo Theories (OMT) and Satisfiability Modulo Theories (SMT), respectively.