Template semantics is a template-based approach to describing the semantics of model-basednotations, where a pre-defined template captures the notations;; common semantics, and parametersspecify 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 theSMV family of model checkers. We describe a fully automated translator that takes as input aspecification written in template semantics syntax, and a set of template parameters, encodingthe specification;;s semantics, and generates an SMV model of the specification. The result is aparameterized technique for model checking specifications written in a variety of notations. Ourwork also shows how to represent complex composition operators, such as rendezvous synchronization,in the SMV language, in which there is no matching language construct.
PDF
download
878987797
028-85220240
