Return to search

Mapping Template Semantics to SMV

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.

Identiferoai:union.ndltd.org:WATERLOO/oai:uwspace.uwaterloo.ca:10012/1205
Date January 2004
CreatorsLu, Yun
PublisherUniversity of Waterloo
Source SetsUniversity of Waterloo Electronic Theses Repository
LanguageEnglish
Detected LanguageEnglish
TypeThesis or Dissertation
Formatapplication/pdf, 980691 bytes, application/pdf
RightsCopyright: 2004, Lu, Yun. All rights reserved.

Page generated in 0.0021 seconds