An important step in model-based embedded system design consists in mapping functional specifications and their tasks/operations onto execution architectures and their ressources. This mapping comprises both temporal scheduling and spatial allocation aspects. Therefore, we promote an approach which starts from loosely-timed/asynchronous models and proceeds by refining them to fully synchronized ones, using so-called clock calculus techniques under the architecture constraints. In this paper we provide a modeling framework based on an intermediate representation format, called clocked graphs, for polychronous endochronous specifications, which are the ones that can be safely considered for deterministic distributed real-time implementation using static scheduling techniques. Our formalism allows the specification of both “intrinsic” correctness properties of the specification, such as causality and clock consistency, and “external” correctness properties, such as endochron...