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.
| Identifer | oai:union.ndltd.org:WATERLOO/oai:uwspace.uwaterloo.ca:10012/1205 |
| Date | January 2004 |
| Creators | Lu, Yun |
| Publisher | University of Waterloo |
| Source Sets | University of Waterloo Electronic Theses Repository |
| Language | English |
| Detected Language | English |
| Type | Thesis or Dissertation |
| Format | application/pdf, 980691 bytes, application/pdf |
| Rights | Copyright: 2004, Lu, Yun. All rights reserved. |
Page generated in 0.0021 seconds