La verificación de los requisitos de seguridad es una tarea importante durante el desarrollo de sistemas críticos de seguridad. La creciente complejidad de los sistemas hace que el análisis manual sea casi imposible. Este documento presenta una nueva metodología para la verificación formal de sistemas técnicos con smartIflow (Máquinas de Estado para la Automatización de Tareas Relacionadas con la Fiabilidad utilizando Flujos de Información). smartIflow es un nuevo lenguaje de modelado que ha sido diseñado especialmente para automatizar el proceso de análisis de seguridad en las primeras etapas del ciclo de vida del producto. Se basa en la experiencia con enfoques existentes. Como es práctica común en los enfoques actuales, los componentes se modelan como máquinas de estado finito. Sin embargo, se introducen nuevos conceptos para describir las interacciones entre componentes. Los eventos juegan un papel importante en las interacciones internas entre componentes, así como en las interacciones externas (del usuario). Nuestro enfoque para la verificación de requisitos de seguridad especificados formalmente es un método de dos pasos. Primero, una simulación exhaustiva crea conocimiento sobre una gran variedad de comportamientos posibles del sistema, incluyendo especialmente reacciones a fallos que ocurren repentinamente (posiblemente intermitentes). En el segundo paso, se verifican los requisitos de seguridad especificados en CTL (Lógica de Árbol de Cálculo) utilizando técnicas de verificación de modelos, y se generan contraejemplos si no se satisfacen. La aplicabilidad práctica de este enfoque se demuestra a partir de una implementación en Java utilizando un simple sistema de Dos Tanques-Bomba-Consumidor.