In the past, techniques for specifying, verifying and implementing protocols have taken on a somewhat ad hoc (non -uniform) and informal nature. This lack of uniformity has resulted in an abundance of techniques and methodologies for analysing protocols, most of which are applicable to protocols having a small degree of complexity. Typically, different techniques are applied to various stages of a protocol development without an underlying formal basis for their integrated application. As a result, there may be no way to guarantee that subsequent stages of a development represent correct realisations of earlier ones. This thesis aims to address the problem of protocol development stated above by describing unified frameworks within which: 1) A formal theoretical foundation is laid for specifying, verifying and implementing protocols. 2) A knowledge based system is used for the formal development of a certain class of protocols. A number of limitations have been identified in the approach taken for developing the frameworks: a) The lack of 'compositional' expressiveness of the algebraic specification language. This makes it difficult to effectively analyse concurrently executing processes of protocols. b) The lack of support provided for addressing performance related issues. This makes it difficult to compare different protocols to assess their effect with respect to how long they take to achieve some data processing task. c) The protocol derivation algorithm can prove cumbersome in its application and may require a significant amount of domain knowledge (about types of 'primitives') in order to be machine automated. d) The knowledge based framework is currently limited to supporting the development of end-to-end protocols. This however is not a serious problem as the ideas and principles applied in developing these protocols form the basis for work in analysing other types. The above limitations form the basis for future work which will aim to address the problems stated. The thesis is in 5 main parts:- I) A description of various formalisms used in the past, to specify protocols. From this analysis, criteria are developed for assessing the relative merits of these formalisms, with a view towards choosing one such technique to be employed in specifying protocols. ii) A formal development of the protocol which includes a discussion of automatic theorem proving via a syntactic measure known as a trace. iii) A description of a notation with operational semantics developed for specifying and verifying protocols and services. In addition, a method utilising the notation is described whereby a service can be derived from a protocol. iv) A description of a framework within which a protocol may be verified in respect of the service it provides. v) A description of an interactive program (environment) allowing the formal development of a certain class of distributed protocols, such as the ECMA application layer protocol. The originality of this work lies in the: I) development of a methodology for automatically deriving and proving invariant properties of a specification. ii) development of a notation with operational semantics, capable of specifying and verifying distributed protocols and services. iii) identification of a means by which the correspondence between a specification and its implementation may be used as rewrite rules (not necessarily preserving all semantic information) in developing communication protocols. v) numerous algorithms described for addressing safety, liveness and conformity issues, as part of the interactive environment.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:278356 |
| Date | January 1990 |
| Creators | Haughton, Howard |
| Publisher | University of Wolverhampton |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
Page generated in 0.0062 seconds