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...
Main Authors: | , |
---|---|
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 |