Funk, Peter J.

2018-01-31T11:44:12Z

2018-01-31T11:44:12Z

1999

The use of formal specifications based on varieties of mathematical logic is becoming common in the process of designing and implementing safety critical systems and practices for hardware design. Formal methods are usually intended to include in the specification, all the important details of the final system in the specification, with the aim of proving that the specification possesses certain properties and lacks other unwanted properties. In large, complex systems, this task requires sophisticated theorem proving, which can be difficult and complicated. Telecommunications systems are large and complex, making detailed formal specification impractical given current technology. However, formal “sketches” of the behaviours the services provide can be produced, and these can be very helpful in locating which service might be relevant to a given problem.

This thesis describes CABS, a case-based approach that uses coarse-grained graphical requirements specification sketches, to outline the basic behaviour of the system's func­tional modules (called services), thereby allowing us to identify, re-use and adapt re­quirements (from cases stored in a library), to construct new cases. The matching algorithm identifies similar behaviour between the input examples and the cases stored in the case library. By using cases that have already been tested, integrated and im ­plemented, less effort is needed to produce requirements specifications on a large scale. Using a hypothetical telecommunications system as an example, it will be shown that a comparatively simple logic can be used to capture coarse-grained behaviour and how a case-based approach benefits from this. The input from the examples is used both to identify the cases whose behaviour corresponds most closely to the designer's intentions, and also in the process of adapting, validating and, finally, verifying the proposed solution against the examples.

http://hdl.handle.net/1842/28076

The University of Edinburgh

Annexe Thesis Digitisation Project 2017 Block 16

Already catalogued

CABS: a case-based and graphical requirements capture, formalisation and verification system

Thesis or Dissertation

PhD Doctor of Philosophy