Semantic Specification and Verification of Data Flow Diagrams

摘要

Data Flow Diagram (DFD) has been widely used in Software Engineering as means of requirement 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 Data Flow Diagram as networks of concurrent processes.With the use of temporal logic language XYZ/E,the formal basis of the semantic specification of DFD can be ensured,and the system properties such 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 verification methodology is proposed and several examples are analyzed.The implementation of the tools which can support the formal specification,verification and simulation of DFD are also briefly described.