Formal specifications are indispensable in the design of verifiable complex distributed systems, and formal methods have received considerable attention in that respect. However, the full potential of formal methods can only be realized if the transition from specification to actual implementation can be automated to preserve the properties that were established and proved in the specification. Tempo is an integrated development environment that implements the Timed Input/Output Automata (TIOA) language and can be used to model and verify distributed, concurrent, and timed systems as collections of interacting state machines. In Tempo, individual software modules are modeled as separate automata, while complex distributed systems are modeled through composition mechanisms. To build and deploy an actual distributed system, one must both derive an implementation that is consistent with the formal specification and solve an optimization problem (often NP-hard) to match the software components with the computing resources within the target network, given criteria such as minimizing the resulting network load. This paper assumes that an implementation is available and focuses on the second problem. Namely, it presents new Tempo features for specifying deployment requirements and automatically solving the resulting optimization problem with constraint programming techniques. The new annotation features describe the target platform as well as satisfiability constraints (e.g., physical separation of the software modules implementing replicas in a distributed data service). The augmented specification is translated into a COMET program to compute the optimal deployment. The current set of annotations handles the minimization of communication cost. The implementation can solve hard instances that are beyond the capabilities of modern mixed-integer programming solvers. The paper illustrates this process using a distributed eventually-serializable data service.