• Login
    View Item 
    •   Home
    • Massey Documents by Type
    • Theses and Dissertations
    • View Item
    •   Home
    • Massey Documents by Type
    • Theses and Dissertations
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    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

    Icon
    View/Open Full Text
    01_front.pdf (167.9Kb)
    02_whole.pdf (3.270Mb)
    Export to EndNote
    Abstract
    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.
    Date
    1989
    Author
    France, Robert Bertrand
    Rights
    The Author
    Publisher
    Massey University
    URI
    http://hdl.handle.net/10179/12810
    Collections
    • Theses and Dissertations
    Metadata
    Show full item record

    Copyright © Massey University
    | Contact Us | Feedback | Copyright Take Down Request | Massey University Privacy Statement
    DSpace software copyright © Duraspace
    v5.7-2023.7-7
     

     

    Information PagesContent PolicyDepositing content to MROCopyright and Access InformationDeposit LicenseDeposit License SummaryTheses FAQFile FormatsDoctoral Thesis Deposit

    Browse

    All of MROCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

    My Account

    LoginRegister

    Statistics

    View Usage Statistics

    Copyright © Massey University
    | Contact Us | Feedback | Copyright Take Down Request | Massey University Privacy Statement
    DSpace software copyright © Duraspace
    v5.7-2023.7-7