Semantic Specification and Verification of Data Flow Diagrams

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.