A unified modeling language framework for specifying and analyzing temporal properties
| dc.contributor.author | Al Lail, Mustafa, author | |
| dc.contributor.author | France, Robert B., advisor | |
| dc.contributor.author | Ray, Indrakshi, advisor | |
| dc.contributor.author | Ray, Indrajit, committee member | |
| dc.contributor.author | Hamid, Idris Samawi, committee member | |
| dc.contributor.author | Malaiya, Yashwant K., committee member | |
| dc.date.accessioned | 2018-09-10T20:05:55Z | |
| dc.date.available | 2018-09-10T20:05:55Z | |
| dc.date.issued | 2018 | |
| dc.description.abstract | 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. | |
| dc.format.medium | born digital | |
| dc.format.medium | doctoral dissertations | |
| dc.identifier | AlLail_colostate_0053A_15099.pdf | |
| dc.identifier.uri | https://hdl.handle.net/10217/191492 | |
| dc.language | English | |
| dc.language.iso | eng | |
| dc.publisher | Colorado State University. Libraries | |
| dc.relation.ispartof | 2000-2019 | |
| dc.rights | Copyright 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. | |
| dc.subject | properties | |
| dc.subject | temporal | |
| dc.subject | verification | |
| dc.subject | specification | |
| dc.subject | model checking | |
| dc.subject | UML | |
| dc.title | A unified modeling language framework for specifying and analyzing temporal properties | |
| dc.type | Text | |
| dcterms.rights.dpla | This Item is protected by copyright and/or related rights (https://rightsstatements.org/vocab/InC/1.0/). 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). | |
| thesis.degree.discipline | Computer Science | |
| thesis.degree.grantor | Colorado State University | |
| thesis.degree.level | Doctoral | |
| thesis.degree.name | Doctor of Philosophy (Ph.D.) |