This thesis proposes a framework, based on formal methods, for the design, specification, and analysis of 1. neurocomputers as seen from the perspective of hardware, and 2. real world tasks as seen from the perspective of a user, in order to give useful definitions of correctness. We apply the theory of synchronous concurrent algorithms to a number of well known neural network models. This gives us a detailed, and precise description of the spatial and temporal behaviour of the network's operation. Such an operational semantics is necessary for defining a notion of correctness for such sytems. In order to formally specify a task and define its correctness we extend the standard treatment of synchronous concurrent algorithm correctness to the case of approximate correctness, and using mathematical tools from universal algebra and topology, examine the semantics of a number of natural 'approximate specifications'. We apply this framework to two case studies: the requirements analysis of a hospital waiting list management system, and the implementation of a hypothetical anti-ballistic missile firing system.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:636706 |
| Date | January 1994 |
| Creators | Yates, W. B. |
| Publisher | Swansea University |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
Page generated in 0.0013 seconds