Towards SMV Model Checking of Signal (multi-clocked) Specifications

Abstract

Signal is a high-level data-flow specification language that equally
allows multi-clocked descriptions as well as single-clocked ones.
It has a formal semantics and is supported by several formal tools for
simulation and static validation.
This generality renders it useful for various specification, simulation, and
verification tasks in embedded system design.
SMV, in turn, is a language and model checker where synchronous models are single-clocked by definition.
Roughly, we use standard techniques to describe clocks by Boolean variables, with the advantage that the number of such variables is kept to a minimum through a static analysis provided by the Signal compiler.
In particular, we propose a translation from possibly multi-clocked
Signal specifications into SMV specifications for their corresponding verification by model checking.