Formal System Design (ForSyDe) aims to bring the design of multiprocessor systems-on-chip (MPSoCs) to a higher level of abstraction and bridge the abstraction gap by transformational design refinement. The current research is focused on a correct-by-construction design flow, which requires design space exploration including formal models of computation and timepredictable platforms. The latter is widely used for hard real-time systems. In order to make a platform time-predictable, all components, as well as inter-core communication, need to have the worst-case execution time (WCET) estimations and be easily analyzed. Time-division multiplexing (TDM) networks can precisely allocate network resources at each time point and further provide tim...