At present, embedded system development establishes embedded component model (ECM) with informal and unstructured methods, and the dependencies among components are implicit and lack rigorous semantic. This paper presents a formal model for specification, verification, and composition of embedded system. In this paper, we provide a rigorous and compact description of the modeling elements of ECM and define component combination operations based on formal semantics which is feasible and effective both theoretically and practically. The corresponding techniques such as component property, connection constraints and ECM hierarchy are also discussed in this paper. Based on this model, DTSED component production toolkit is developed as the support platform for the ECM. Finally, a case study is introduced to explain how the above ECM can be used.