UWSpace is currently experiencing technical difficulties resulting from its recent migration to a new version of its software. These technical issues are not affecting the submission and browse features of the site. UWaterloo community members may continue submitting items to UWSpace. We apologize for the inconvenience, and are actively working to resolve these technical issues.
 

Mapping Template Semantics to SMV

Thumbnail Image

Files

y4lu2004.pdf (957.71 KB)

Date

2004

Authors

Lu, Yun

Journal Title

Journal ISSN

Volume Title

Publisher

University of Waterloo

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.

Description

Keywords

Computer Science, Formal Methods, Model Checking

LC Keywords

Citation

URI

http://hdl.handle.net/10012/1205

Collections

Theses
Computer Science