A formal framework for analyzing sequence diagram

Simple item page
dc.contributor.advisorNiu, Jianwei
dc.contributor.authorShen, Hui
dc.contributor.committeeMemberNiu, Jianwei
dc.contributor.committeeMembervon Ronne, Jeffery
dc.contributor.committeeMemberZhang, Weining
dc.contributor.committeeMemberZhu, Dakai
dc.contributor.committeeMemberKrishnan, Ram
dc.date.accessioned2024-03-08T15:44:52Z
dc.date.available2024-03-08T15:44:52Z
dc.date.issued2013
dc.descriptionThis item is available only to currently enrolled UTSA students, faculty or staff. To download, navigate to Log In in the top right-hand corner of this screen, then select Log in with my UTSA ID.
dc.description.abstractGraphical representations of scenarios, such as UML Sequence Diagrams, 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 Sequence Diagram permit different types of control flows, including interleaving, alternative, and loop, for representing complex and concurrent behaviors. These fragments increase a Sequence Diagram's expressiveness, yet introduce a challenge to comprehend what behavior is possible in the traces that express system executions. Furthermore, software practitioners tend to use a collection of Sequence Diagrams to express multiple usages of a software system. It can be extremely difficult to determine manually that multiple Sequence Diagrams constitute a consistent, correct specification. This dissertation introduces an approach to codify the semantics of Sequence Diagrams with Combined Fragments in terms of Linear Temporal Logic (LTL) templates. In each template, different semantic aspects are expressed as separate, yet simple LTL formulas that can be composed to define the semantics of all the Combined Fragments. In addition, we develop an approach to transform Sequence Diagrams with Combined Fragments into the input language of model checker NuSMV. The analytical powers of model checking can be leveraged to automatically determine if a collection of Sequence Diagrams is consistent. Another benefit of this approach is the ability to specify certain safety properties of a system as intuitive Sequence Diagrams. We have developed tools to translate Sequence Diagrams to both LTL and NuSMV's input language to demonstrate that they can be automatically verified. We validate our techniques by analyzing two design examples taken from an insurance industry software application. We also model Health Insurance Portability and Accountability Act of 1996 (HIPAA) Privacy Rule using Sequence Diagrams to show that high-level policies can be described using Sequence Diagrams.
dc.description.departmentComputer Science
dc.format.extent207 pages
dc.format.mimetypeapplication/pdf
dc.identifier.isbn9781303114366
dc.identifier.urihttps://hdl.handle.net/20.500.12588/5746
dc.languageen
dc.subject.classificationComputer science
dc.titleA formal framework for analyzing sequence diagram
dc.typeThesis
dc.type.dcmiText
dcterms.accessRightspq_closed
thesis.degree.departmentComputer Science
thesis.degree.grantorUniversity of Texas at San Antonio
thesis.degree.levelDoctoral
thesis.degree.nameDoctor of Philosophy

Files

Original bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
Shen_utsa_1283D_11043.pdf
Size:
1.07 MB
Format:
Adobe Portable Document Format
Download

Collections

Electronic Theses and Dissertations - UTSA Access Only