To meet required real-time constraints, modern embedded systems have to perform many tasks in parallel and therefore require the modeling of concurrent systems with an adequate notion of time. To this end, several models of computation (MoCs) have been defined that determine why (causality), when (time), which atomic action of the system is executed. The most important classes of MoCs are event-triggered, time/clock-triggered, and data-driven MoCs that have their on advantages and disadvantages. This talk gives an overview on the design flow used in the Averest system developed at the University of Kaiserslautern. The heart of this design flow is a synchronous (clock-driven) MoC which is used for modeling, simulation, and formal verification. The use of a synchronous MoC offers many advantages for these early design phases. For the synthesis, however, it is for some target architectures difficult to maintain the synchronous MoC, and therefore transformations are applied to translate the original models into other MoCs. In particular, we consider transformations that allow developers to desynchronize the system into asynchronous components which is a new technique to synthesize distributed/multithreaded systems from verified synchronous models.