A Unified Systems Development Paradigm Which Synthesises Object-Oriented Methodologies and VDM

PhD Thesis


Charatan, Quentin (1996). A Unified Systems Development Paradigm Which Synthesises Object-Oriented Methodologies and VDM . PhD Thesis South Bank University School of Electrical, Electronic and Information Engineering https://doi.org/10.18744/lsbu.96698
AuthorsCharatan, Quentin
TypePhD Thesis
Abstract

This work describes a methodology for systems development whereby the techniques of object-oriented analysis and design are synthesised with those of VDM, a formal development method. The methodology involves the use of Object-Oriented Analysis to derive an Object-Oriented/VDM specification; this specification is then used as the basis for a design technique which synthesises object methods with the formal development techniques of VDM, namely Data Reification and Operation Decomposition.
The work shows that all the important concepts which together define Object-Orientation can be captured in VDM. It demonstrates how the notion of encapsulation can be represented by the use of the VDM module; how inheritance relationships can be represented by means of the module import and export sections; how message-passing between objects can be specified by the quoting of pre- and post-conditions; and how polymorphic relationships can be represented by the use of the parameterised module notation of VDM.
The work also shows how the behaviour of inherited classes can be proved to be consistent by the application of VDM proof obligations.
It is intended that this methodology should make formal methods more accessible to the practitioner, since it does not involve adaptations to the language, but rather demonstrates that the existing VDM development methods easily lend themselves to use in an object-oriented world.

Year1996
PublisherLondon South Bank University
Digital Object Identifier (DOI)https://doi.org/10.18744/lsbu.96698
File
License
File Access Level
Open
Publication dates
Print1996
Publication process dates
Deposited01 Mar 2024
Permalink -

https://openresearch.lsbu.ac.uk/item/96698

Download files


File
1996_PhD_Charatan.pdf
License: CC BY 4.0
File access level: Open

  • 4
    total views
  • 0
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as