Kruti Shah

Date of Award

August 2024

Document Type

Dissertation

Degree Name

Doctor of Philosophy (PhD)

Department

Computer Science

First Advisor

Emanuel S. Grant

Abstract

The Unified Modeling Language (UML) is a foundation in software development, providing standardized notation for visualizing, specifying, constructing, and documenting software systems. UML class models, in particular, offer a static view of a system's structure, capturing essential elements such as classes, attributes, operations, and relationships. Despite the widespread adoption of UML and its class modeling capabilities, challenges persist in ensuring the models' correctness, reliability, and effectiveness. This research presents a comprehensive study of UML's role in software development, delving into existing literature to examine the development of UML class models, its significance in various stages of the software development lifecycle, and the challenges encountered in class modeling. Previous studies have highlighted the utility of UML class models in requirements analysis, design, and documentation, emphasizing its ability to facilitate communication among stakeholders and improve software quality. However, challenges related to incorrectly designed model constructs such as cyclic dependencies, inheritance relationships, and model consistency have been identified as barriers to realizing the full potential of UML class models. A critical analysis of existing research reveals a gap in methodologies for effectively verifying and validating UML class models, particularly in addressing complex design issues and ensuring model correctness. This research fills this gap by proposing a systematic methodology for verifying and validating UML class models, incorporating formal methods and techniques to address common design pitfalls and enhance model reliability. The study employed Object Constraint Language (OCL) formal methods and the Unified Specification Environment (USE) tool to enhance the clarity, consistency, and reliability of class models. It includes the development of a structured methodology and its application to a real-world case study in the safety-critical system domain, specifically the Traffic Collision Avoidance System (TCAS). The result of this study is a verified and validated UML class model for the TCAS. This class model has been meticulously developed through a multi-stage process, including requirement elicitation, class model design, cycle and inheritance relationship removal, and the application of formal methods using OCL and the USE tool. The final TCAS class model demonstrates compliance with safety-critical requirements, ensuring its reliability and correctness. Through iterative refinement and validation, the methodology has effectively enhanced the security and safety of the TCAS system, providing a robust framework for developing reliable safety-critical systems.

Download

Share

COinS