UCT CS Research Document Archive

Analysis of Structured Use Case Models through Model Checking

Ryndina, Ksenia and Pieter Kritzinger (2005) Analysis of Structured Use Case Models through Model Checking. Technical Report CS05-02-00, Department of Computer Science, University of Cape Town.

Full text available as:
PDF - Requires Adobe Acrobat Reader or other PDF viewer.


Inadequate requirements specification remains to be one of the predominant causes of software development project failure today. This is mainly due to the lack of suitable processes, techniques and automated tool support available for specifying and analysing system requirements. In this paper we suggest a way to improve the approach to requirements specification that is the most popular at the moment - use case modelling. Despite their popularity, use case models are not adequate for creating comprehensive and precise requirements specifications. We amend the traditional use case metamodel such that more formal and structured models can be built. Further, we define several analysis schemes for these structured use case models that assist in discovering inconsistencies and other errors in the models. These analysis schemes are automated in a tool that we developed called the Structured Use case Model Analyser (SUM Analyser). The SUM Analyser provides an accessible interface that allows the user to construct use case models, configure and execute several analysis options and view the produced results. The existing NuSMV model checker is used to perform the actual verification tasks for the analysis. To facilitate this, the SUM Analyser transforms use case models to NuSMV programs and also interprets the produced results so that they can be understood by the user.

EPrint Type:Departmental Technical Report
ID Code:220
Deposited By:Arnab, A
Deposited On:22 September 2005