dc.contributor.author | Lu, Yun | en |
dc.date.accessioned | 2006-08-22 14:27:49 (GMT) | |
dc.date.available | 2006-08-22 14:27:49 (GMT) | |
dc.date.issued | 2004 | en |
dc.date.submitted | 2004 | en |
dc.identifier.uri | http://hdl.handle.net/10012/1205 | |
dc.description.abstract | Template 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 | application/pdf | en |
dc.format.extent | 980691 bytes | |
dc.format.mimetype | application/pdf | |
dc.language.iso | en | en |
dc.publisher | University of Waterloo | en |
dc.rights | Copyright: 2004,
Lu, Yun. All rights reserved. | en |
dc.subject | Computer Science | en |
dc.subject | Formal Methods | en |
dc.subject | Model Checking | en |
dc.title | Mapping Template Semantics to SMV | en |
dc.type | Master Thesis | en |
dc.pending | false | en |
uws-etd.degree.department | School of Computer Science | en |
uws-etd.degree | Master of Mathematics | en |
uws.contributor.advisor | Day, Nancy | |
uws.typeOfResource | Text | en |
uws.peerReviewStatus | Unreviewed | en |
uws.scholarLevel | Graduate | en |