Analyzing data flow diagrams by combination of formal methods and visualization techniques

Data flow diagram (DFD) is an indispensable method to model data processing in software engineering. To analyze DFD rigorously, a formal semantics is demanded. Formal interpretation of DFD and its formal semantics lead to an accurate and non-ambiguous analysis. Calculus of Communicating System (CCS), a formal approach in concurrent system modeling, could be utilized to describe DFD. Given its CCS description, automation tools generate the state space of the system depicted by DFD, which reflects all the behaviors of the system. However, analyzing the state space only with character expressions is hard for software developers. In this paper, a visual system is introduced to assist developers to analyze and compare the systems by combination of formal methods and visualization techniques.