You are required to read and agree to the below before accessing a full-text version of an article in the IDE article repository.

The full-text document you are about to access is subject to national and international copyright laws. In most cases (but not necessarily all) the consequence is that personal use is allowed given that the copyright owner is duly acknowledged and respected. All other use (typically) require an explicit permission (often in writing) by the copyright owner.

For the reports in this repository we specifically note that

  • the use of articles under IEEE copyright is governed by the IEEE copyright policy (available at http://www.ieee.org/web/publications/rights/copyrightpolicy.html)
  • the use of articles under ACM copyright is governed by the ACM copyright policy (available at http://www.acm.org/pubs/copyright_policy/)
  • technical reports and other articles issued by M‰lardalen University is free for personal use. For other use, the explicit consent of the authors is required
  • in other cases, please contact the copyright owner for detailed information

By accepting I agree to acknowledge and respect the rights of the copyright owner of the document I am about to access.

If you are in doubt, feel free to contact webmaster@ide.mdh.se

CABS: A Case-Based and Graphical Requirements Capture, Formalisation and Verification System

Authors:


Publication Type:

Doctoral Thesis

Venue:

University of Edinburgh, Scotland

Publisher:

University of Edinburgh


Abstract

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 systems functional modules (called services), thereby allowing us to identify, re-use and adapt requirements (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 implemented, 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 designers intentions, and also in the process of adapting, validating and, finally, verifying the proposed solution against the examples.

Bibtex

@phdthesis{Funk61,
author = {Peter Funk},
title = {CABS: A Case-Based and Graphical Requirements Capture, Formalisation and Verification System},
month = {March},
year = {1998},
school = {University of Edinburgh},
url = {http://www.es.mdu.se/publications/61-}
}