Towards SMV Model Checking of Signal (multi-clocked) Specifications - Peralta, Julio; Gautier, Thierry (Electronic Communications of the EASST, 2009)
Signal is a high-level data-flow specification language that equallyallows multi-clocked descriptions as well as single-clocked ones.It has a formal semantics and is supported by several formal tools forsimulation and static validation.This generality renders it useful for various specification, simulation, andverification 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-clockedSignal specifications into SMV specifications for their corresponding verification by model checking.