Data Flow Diagram(DFD)has been widely used in Software Engineering as means of require-ment analysis and system specification.However,one defect of DFD approach remains untackled:the lack of formal semantics has brought about a lot of problems.In this paper,we model DataFlow Diagram as networks of concurrent processes.With the use of temporal logic languageXYZ/E,the formal basis of the semantic specification of DFD can be ensured,and the system prop-erties sach as safety and liveness can be easily characterized.The main part of this paper is devotedto the study of the hierarchical decomposition of semantic specification and its correctness.A verifica-tion methodology is proposed and several examples are analyzed.The implementation of the toolswhich can support the formal specification,verification and simulation of DFD are also briefly des-cribed. Data Flow Diagram (DFD) has been widely used in Software Engineering as means of require-ment analysis and system specification. Yet, one defect of DFD approach remains untackled: the lack of formal semantics has brought a lot of problems.In this paper , we model DataFlow Diagram as networks of concurrent processes. The use of temporal logic language XYZ / E, the formal basis of the semantic specification of DFD can be ensured, and the system prop-erties sach as safety and liveness can be easily characterized. The main part of this paper is devoted to the study of the hierarchical decomposition of semantic specification and its correctness. A verifica-tion methodology is proposed and several examples are analyzed. The implementation of the toolswhich can support the formal specification, verification and simulation of DFD are also short des-cribed.