Model-to-Model Transformations for Efficient Time-domain Verification of Concurrent Models by NuSMV Modules

Artículo académico que presenta una transformación algorítmica de arreglos LLFSM a módulos NuSMV mediante una transformación ATL de modelo a modelo. La propuesta mejora la eficiencia en la construcción y verificación de modelos, incluyendo predicados temporales, y produce archivos concisos que facilitan la verificación formal, reduciendo significativamente el tamaño de los modelos en comparación con transformaciones anteriores.