Semantically Extended Data Flow Diagrams: A Formal Specification Tool.

The popularity of the Data Flow Diagram (DFD) specification tool in industry seems to stems from its use of intuitively defined concepts and notation. The use of such concepts and notation gives flexibility to the tool and most often results in intuitively appealing specifications. The flexibility comes at a price—the lack of a formal basis for DFD concepts and notation prohibits its use as a formal specification tool. On the other hand, a problem commonly stated as a deterrent to the use of formal specification techniques in industry is the lack of intuitive appeal in the specifications, which has led some researchers to suggest that formal specifications be supplemented with less formal, more intuitive documentations of specified functionalities. In this paper we describe a method for associating a DFD with a formal specification. The intention is to enhance the use of the DFD as a formal specification tool, thus gaining a tool that can be used to document application functionality in an understandable manner and, at the same time, be capable of producing a formal specification that can be used to rigorously investigate semantic properties of the application. [ABSTRACT FROM AUTHOR]