Al Lail, Mustafa, authorFrance, Robert B., advisorRay, Indrakshi, advisorRay, Indrajit, committee memberHamid, Idris Samawi, committee memberMalaiya, Yashwant K., committee member2018-09-102018-09-102018https://hdl.handle.net/10217/191492In 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.born digitaldoctoral dissertationsengCopyright and other restrictions may apply. User is responsible for compliance with all applicable laws. For information about copyright law, please see https://libguides.colostate.edu/copyright.propertiestemporalverificationspecificationmodel checkingUMLText