A Logical Framework for Sequence Diagram with Combined Fragments

dc.contributor.authorShen, Hui
dc.contributor.authorRobinson, Mark
dc.contributor.authorNiu, Jianwei
dc.date.accessioned2023-10-26T15:04:57Z
dc.date.available2023-10-26T15:04:57Z
dc.date.issued2011-11
dc.description.abstractGraphical representations of scenarios, such as UML Sequence Diagrams and Message Sequence Charts, serve as a well-accepted means for modeling the interactions among software systems and their environment through the exchange of messages. The Combined Fragments of UML Sequence Diagram permit various types of control flow among messages (e.g., interleaving and branching) to express an aggregation of multiple traces encompassing complex and concurrent behaviors. However, Combined Fragments increase the difficulty of Sequence Diagram comprehension and analysis. This paper introduces an approach to formalizing the semantics of Sequence Diagrams with Combined Fragments in terms of Linear Temporal Logic (LTL) templates. In all the templates, different semantic aspects are expressed as separate, yet simple LTL formulas that can be composed to define the semantics of basic Sequence Diagram, all the Combined Fragments, and nested Combined Fragments. Moreover, the formalization enables us to leverage the analytical powers of automated decision procedures for LTL formulas to determine if a collection of Sequence Diagrams is consistent, safe, and deadlock-free.
dc.description.departmentComputer Science
dc.identifier.urihttps://hdl.handle.net/20.500.12588/2178
dc.language.isoen_US
dc.publisherUTSA Department of Computer Science
dc.relation.ispartofseriesTechnical Report; CS-TR-2011-015
dc.subjectmodeling
dc.subjectformal analysis
dc.subjectsequence diagram
dc.subjectconcurrency and communication
dc.subjecttemporal logic
dc.titleA Logical Framework for Sequence Diagram with Combined Fragments
dc.typeTechnical Report

Files

Original bundle

Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Shen_et_al_CS-TR-2011-015.pdf
Size:
1.34 MB
Format:
Adobe Portable Document Format

License bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.86 KB
Format:
Item-specific license agreed upon to submission
Description: