Show simple item record

dc.contributor.authorLu, Yunen 14:27:49 (GMT) 14:27:49 (GMT)
dc.description.abstractTemplate semantics is a template-based approach to describing the semantics of model-based notations, where a pre-defined template captures the notations' common semantics, and parameters specify the notations' distinct semantics. In this thesis, we investigate using template semantics to parameterize the translation from a model-based notation to the input language of the SMV family of model checkers. We describe a fully automated translator that takes as input a specification written in template semantics syntax, and a set of template parameters, encoding the specification's semantics, and generates an SMV model of the specification. The result is a parameterized technique for model checking specifications written in a variety of notations. Our work also shows how to represent complex composition operators, such as rendezvous synchronization, in the SMV language, in which there is no matching language construct.en
dc.format.extent980691 bytes
dc.publisherUniversity of Waterlooen
dc.rightsCopyright: 2004, Lu, Yun. All rights reserved.en
dc.subjectComputer Scienceen
dc.subjectFormal Methodsen
dc.subjectModel Checkingen
dc.titleMapping Template Semantics to SMVen
dc.typeMaster Thesisen
dc.pendingfalseen of Computer Scienceen
uws-etd.degreeMaster of Mathematicsen
uws.contributor.advisorDay, Nancy

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