Status: open
Improving TSNsched, a SMT based auto gate scheduler
PA: Research Project (INF-PM-FPA / INF-PM-FPG) or
BA: Bachelor Thesis (or Studienarbeit / Großer Beleg) or
MA: Master's Thesis (or Diploma Thesis / Diplomarbeit)
Creating a network schedule is a hard (even NP-hard) problem. To do this in an automated way, auto gate schedulers are used. One open source implementation is TSNsched, which is written in Java and internally uses Z3, a SMT solver developed by Microsoft. Although TSNsched is capable of generating basic schedules, it is not actively maintained. This leads to some missing features and potential for improvements, especially regarding the ongoing improvement of Z3.
Goals of the thesis
This thesis aims to improve TSNsched and make it more suitable for scheduling in a vehicular context. Some examples could be the flow generation process to support time-triggered flows, finding potential improvements regarding the use of Z3, or solving the problem of creating new schedules during an ongoing schedule cycle. This will be applied to existing TSN implementations in INET, which uses TSNsched to dynamically generate schedules at runtime.
Based on the type of the thesis the requirements may be adjusted.
Requirements
- Experience with Java and C++