Formal Analysis Of Use Case Diagrams

Use case diagrams play an important role in modeling with UML. Careful modeling is crucialin obtaining a correct and efficient system architecture. The paper refers to the formalanalysis of the use case diagrams. A formal model of use cases is proposed and its constructionfor typical relationships b...

Full description

Bibliographic Details
Main Authors: Radosław Klimek, Piotr Szwed
Format: Article
Language:English
Published: AGH University of Science and Technology Press 2010-01-01
Series:Computer Science
Subjects:
Online Access:http://journals.agh.edu.pl/csci/article/download/117/66
id doaj-6d13b88d446f4ffabcf1ac6758cf5470
record_format Article
spelling doaj-6d13b88d446f4ffabcf1ac6758cf54702020-11-24T23:12:10ZengAGH University of Science and Technology PressComputer Science1508-28062010-01-011111510.7494/csci.2010.11.0.115Formal Analysis Of Use Case DiagramsRadosław Klimek0Piotr Szwed1AGH University of Science and TechnologyAGH University of Science and TechnologyUse case diagrams play an important role in modeling with UML. Careful modeling is crucialin obtaining a correct and efficient system architecture. The paper refers to the formalanalysis of the use case diagrams. A formal model of use cases is proposed and its constructionfor typical relationships between use cases is described. Two methods of formal analysis andverification are presented. The first one based on a states’ exploration represents a modelchecking approach. The second one refers to the symbolic reasoning using formal methodsof temporal logic. Simple but representative example of the use case scenario verification isdiscussed.http://journals.agh.edu.pl/csci/article/download/117/66UML; use case; formal model; verification; model checking; temporal logic; semantic tableau
collection DOAJ
language English
format Article
sources DOAJ
author Radosław Klimek
Piotr Szwed
spellingShingle Radosław Klimek
Piotr Szwed
Formal Analysis Of Use Case Diagrams
Computer Science
UML; use case; formal model; verification; model checking; temporal logic; semantic tableau
author_facet Radosław Klimek
Piotr Szwed
author_sort Radosław Klimek
title Formal Analysis Of Use Case Diagrams
title_short Formal Analysis Of Use Case Diagrams
title_full Formal Analysis Of Use Case Diagrams
title_fullStr Formal Analysis Of Use Case Diagrams
title_full_unstemmed Formal Analysis Of Use Case Diagrams
title_sort formal analysis of use case diagrams
publisher AGH University of Science and Technology Press
series Computer Science
issn 1508-2806
publishDate 2010-01-01
description Use case diagrams play an important role in modeling with UML. Careful modeling is crucialin obtaining a correct and efficient system architecture. The paper refers to the formalanalysis of the use case diagrams. A formal model of use cases is proposed and its constructionfor typical relationships between use cases is described. Two methods of formal analysis andverification are presented. The first one based on a states’ exploration represents a modelchecking approach. The second one refers to the symbolic reasoning using formal methodsof temporal logic. Simple but representative example of the use case scenario verification isdiscussed.
topic UML; use case; formal model; verification; model checking; temporal logic; semantic tableau
url http://journals.agh.edu.pl/csci/article/download/117/66
work_keys_str_mv AT radosławklimek formalanalysisofusecasediagrams
AT piotrszwed formalanalysisofusecasediagrams
_version_ 1725602101800730624