A formal framework for data flow diagrams with control extensions : a dissertation presented in partial fulfilment of the requirements for the degree of Doctor of Philosophy in Computer Science at Massey University

In this thesis a formal foundation for data flow diagrams (DFDs) with control extensions is developed. The DFD is the primary specification tool of the Structured Analysis (SA) approach to requirements analysis and specification. In recent times, a number of extensions to DFDs, which enhance their use in the specification of behaviour of complex applications (i.e. applications with concurrent or real-time aspects), have been proposed. Such extensions tend to concentrate on increasing the descriptive power of DFDs, while paying less attention to providing the extended DFDs with a formal foundation. Such a foundation would facilitate the generation of formal specifications from DFDs, which could then be used to rigorously validate the DFDs and the behavioural properties they capture, and could also be used as the basis of formal verification activities where subsequent specifications are verified against the formal specifications generated from DFDs. Also, the simple, graphical nature of DFDs, supported by a formal foundation, facilitates their use in formal development strategies. Their use in this respect achieves a level of understandability not usually associated with formal specification tools. The formal foundation introduced in this thesis consists of two parts: the Picture Level (PL) and the Specification Level (SL). The PL is an algebraic specification characterizing the syntactic aspects of DFDs. The specification is associated with an operational semantics which provides an effective means for investigating the syntactic properties of DFDs with the PL. The SL consists of tools and techniques for describing control aspects of applications, and for formally specifying the data, functional, and control aspects of the control-extended DFDs. The control-extended DFDs are called Extended DFDs (ExtDFDs). An ExtDFD depicts the types of interactions that can take place between DFD components, as well as the events that affect the mode of operation of the application it models. A formal specification, called the Behavioural Specification (BS), is generated from an ExtDFD and supporting specifications characterizing the data objects and primitive processing components of the ExtDFD. The role of the BS in formal validation and verification activities is discussed in this thesis