Repository logo

A unified modeling language framework for specifying and analyzing temporal properties

dc.contributor.authorAl Lail, Mustafa, author
dc.contributor.authorFrance, Robert B., advisor
dc.contributor.authorRay, Indrakshi, advisor
dc.contributor.authorRay, Indrajit, committee member
dc.contributor.authorHamid, Idris Samawi, committee member
dc.contributor.authorMalaiya, Yashwant K., committee member
dc.description.abstractIn the context of Model-Driven Engineering (MDE), designers use the Unified Modeling Language (UML) to create models that drive the entire development process. Once UML models are created, MDE techniques automatically generate code from the models. If the models have undetected faults, they are propagated to code where they require considerable time and effort to detect and correct. It is therefore mandatory to analyze UML models at earlier stages of the development life-cycle to ensure the success of the MDE techniques in producing reliable software. One approach to uncovering design errors is to formally specify and analyze the properties that a system has to satisfy. Although significant research appears in specifying and analyzing properties, there is not an effective and efficient UML-based framework that specifies and analyzes temporal properties. The contribution of this dissertation is a UML-based framework and tools for aiding UML designers to effectively and efficiently specify and analyze temporal properties. In particular, the framework is composed of 1) a UML specification technique that designers can use to specify temporal properties, 2) a rigorous analysis technique for analyzing temporal properties, 3) an optimization technique to scale the analysis to large class models, and 4) a proof-of-concept tool. An evaluation of the framework using two real-world studies shows that the specification technique can be used to specify a variety of temporal properties and the analysis technique can uncover certain types of design faults. It also demonstrates that the optimization technique can significantly speed up the analysis.
dc.format.mediumborn digital
dc.format.mediumdoctoral dissertations
dc.publisherColorado State University. Libraries
dc.rightsCopyright and other restrictions may apply. User is responsible for compliance with all applicable laws. For information about copyright law, please see
dc.subjectmodel checking
dc.titleA unified modeling language framework for specifying and analyzing temporal properties
dcterms.rights.dplaThis Item is protected by copyright and/or related rights ( You are free to use this Item in any way that is permitted by the copyright and related rights legislation that applies to your use. For other uses you need to obtain permission from the rights-holder(s). Science State University of Philosophy (Ph.D.)


Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
6.32 MB
Adobe Portable Document Format