Mapping Template Semantics to SMV

Loading...
Thumbnail Image

Date

2004

Authors

Lu, Yun

Advisor

Day, Nancy

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 Subject Headings

Citation