Resumen

(GSTE) es una extensión de la evaluación de trayectorias simbólicas (STE) y un método de verificación de modelos. Las especificaciones de GSTE se presentan como grafos de afirmaciones. Hay cuatro métodos eficientes para verificar si un modelo de circuito cumple con un grafo de afirmaciones en GSTE, Verificación de Modelos de Satisfacibilidad Fuerte (SMC), Verificación de Modelos de Satisfacibilidad Normal (NMC), Verificación de Modelos de Satisfacibilidad Justa (FMC) y Verificación de Modelos de Satisfacibilidad Terminal (TMC). SMC, NMC y FMC han sido probados y aplicados en la industria, pero TMC no lo ha sido. Este documento presenta una definición de seis tuplas y un nuevo algoritmo para TMC. Basándonos en esto, demostramos que nuestro algoritmo es sólido y completo. Resuelve la limitación de SMC (resultando en falsos negativos) sin extenderse de una especificación finita a una especificación infinita. Por último, se logra un caso de uso de TMC

• Materias:Modelos matemáticos Conjuntos difusos Ecuaciones integrales Fusión de características Algoritmo de optimización
• Subjects:Mathematical models Fuzzy sets Integral equations Feature fusion Optimization algorithm
• Palabras claves:Extensión; Evaluación de trayectoria simbólica; Verificación de modelos; Grafos de afirmaciones; Métodos eficientes; Modelo de circuito
• Keywords:Extension; Symbolic trajectory evaluation; Model checking; Assertion graphs; Efficient methods; Circuit model