Lu, Yun2006-08-222006-08-2220042004http://hdl.handle.net/10012/1205Template 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.application/pdf980691 bytesapplication/pdfenCopyright: 2004, Lu, Yun. All rights reserved.Computer ScienceFormal MethodsModel CheckingMaster Thesis