Repository logo

Theses and Dissertations

Permanent URI for this collection

https://hdl.handle.net/10217/100389

Browse

Browsing Theses and Dissertations by Author "Al Lail, Mustafa, author"

Now showing 1 - 1 of 1
  • Thumbnail Image
    ItemOpen Access
    A unified modeling language framework for specifying and analyzing temporal properties
    (Colorado State University. Libraries, 2018) Al Lail, Mustafa, author; France, Robert B., advisor; Ray, Indrakshi, advisor; Ray, Indrajit, committee member; Hamid, Idris Samawi, committee member; Malaiya, Yashwant K., committee member
    In 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.