Mapping big-step modeling languages to SMV

Abstract

We propose an algorithm for creating a semantics-based, parameterized translator from the family of big-step modelling languages (BSMLs) to the input language of the model checker SMV. Our translator takes as input a specification in the CHTS notation and a set of user-provided parameters that encode the specification's semantics; it produces an SMV model suitable for model checking. We use a modular approach for translation, which means that the structure of the resulting SMV model matches the source CHTS structure.