Resumen

La eficiencia de la verificación composicional de invariantes depende de la abstracción, lo que puede llevar a una verificación incompleta. En este artículo se proponen técnicas de fortalecimiento de invariantes y particionamiento de estados. El primero podría refinar la sobreaproximación eliminando los estados inalcanzables, y el segundo es una variante del refinamiento de abstracción guiado por contraejemplos. Integrado con estas dos técnicas de refinamiento, se presenta un marco unificado de verificación composicional para fortalecer la abstracción y encontrar contraejemplos. Se incluyen algunos ejemplos para mostrar que la verificación de las propiedades de seguridad en sistemas basados en componentes ha sido lograda por nuestro marco.

• 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:Eficiencia; Verificación composicional; Invariantes; Abstracción; Contraejemplos; Propiedades de seguridad
• Keywords:Efficiency; Compositional verification; Invariants; Abstraction; Counterexamples; Safety properties