Transformational design is aformal technique directed at design correctness. It integrates design and veriJication by the use of pre-proven behaviour preserving transformations as design steps. A formal framework is necessary but hidden for the designer. Five formal aspects are integrated in the presented formal framework that is aimed at the design of complex systems composed out of different kinds of subsystems. The tagged signal model is used as "eta' model for a heterogeneous set of computational models with different concurrency semantics. The offered possibilities of model rejnement by transformations and the ability to incorporate heterogeneity are valuable extensions with respect to other transformational design approaches for high-level synthesis.