Es importante verificar tanto la corrección como las propiedades en tiempo real de los sistemas embebidos. Sin embargo, dado que los programas informáticos prácticos están representados por sistemas de transición de estados infinitos, especificar y verificar un programa informático es difícil. Las propiedades en tiempo real también son importantes para los programas embebidos, pero verificar las propiedades en tiempo real de un programa embebido es difícil. En este documento, nos enfocamos en verificar un programa de ensamblaje embebido, con el fin de verificar las propiedades de seguridad en tiempo real. Proponemos un método de verificación deductiva para verificar las propiedades de seguridad en tiempo real, basado en tiempo discreto, de la siguiente manera: (1) Primero, construimos un modelo computacional temporal que incluye el tiempo de ejecución del programa de ensamblaje. Podemos especificar un sistema de transición de estados infinitos que incluya el tiempo de ejecución del modelo computacional temporal. (2) Luego, verificamos si un modelo computacional temporal satisface fórmulas de LTL en tiempo real (Lógica Temporal Lineal en Tiempo Real) mediante verificación deductiva. Podemos especificar propiedades en tiempo real mediante LTL en tiempo real. Con nuestros métodos propuestos, podemos lograr la verificación de las propiedades de seguridad en tiempo real de un programa embebido.