Show simple item record

dc.contributor.authorTanuan, Meyer C.en 14:21:11 (GMT) 14:21:11 (GMT)
dc.description.abstractThe 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.en
dc.format.extent481369 bytes
dc.publisherUniversity of Waterlooen
dc.rightsCopyright: 2001, Tanuan, Meyer C.. All rights reserved.en
dc.subjectComputer Scienceen
dc.subjectObject-Oriented Software Specificationen
dc.subjectModel Checkingen
dc.titleAutomated Analysis of Unified Modeling Language (UML) Specificationsen
dc.typeMaster Thesisen
dc.pendingfalseen of Computer Scienceen
uws-etd.degreeMaster of Mathematicsen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages