Automated Analysis of Unified Modeling Language (UML) Specifications
Meyer Tanuan · UWSpace (University of Waterloo) · 2001
I hereby declare that I am the sole author of this thesis. This is a true copy of the thesis, including any required final revisions, as accepted by my examiners. I understand that my thesis may be made electronically available to the public. ii The Unified Modeling Language (UML) is a standard language adopted by the Object Management Group (OMG) for writing object-oriented (OO) descriptions of software systems. UML allows the analyst to add class-level and system-level constraints. However, UML does not describe how to check the correctness of these constraints. Recent studies have shown that Symbolic Model Checking can effectively verify large software specifications. In this thesis, we investigate how to use model checking to verify constraints of UML specifications. We describe the process of specifying, translating and verifying UML specifications for an elevator example. We use the Cadence Symbolic Model Verifier (SMV) to verify the system properties. We demonstrate how to write a UML specification that can be easily translated to SMV. We propose a set of rules and guidelines to translate UML specifications to SMV, and then use these to translate a non-trivial UML elevator specification to SMV. We look at errors detected throughout the specification, translation and verification process, to see how well they reveal errors, ambiguities and omissions in the user requirements. iii Acknowledgements I would like to thank my supervisor, Dr. Joanne M. Atlee, for her valuable comments and insightful suggestions. I am very grateful for her encouragement and guidance throughout this work. To Professor Dan Berry, I thank him for pointing out that some of the errors revealed during model checking were requirements-level errors. I also thank my thesis reader, Dr. Nancy Day, who provided a thorough review of my thesis. I highly appreciate her detailed and helpful comments. Finally, I thank Doug Guderian for acting as our domain expert for the elevator case study. iv v To my wife,