Revisión sistemática a la literatura para determinar los enfoques de la investigación en verificación formal del software
Resumen
Ubicación en Biblioteca USB Medellín (San Benito): CD-1922t. La verificación tradicional se ha convertido en el cuello de botella en el flujo de diseño de sistemas de gran complejidad. La simulación de los diseños es muy costoso en términos de tiempo y la simulación exhaustiva es prácticamente imposible. Como resultado, los diseñadores han recurrido a métodos formales para la verificación. La verificación formal garantiza una cobertura total del espacio de estados de todo el diseño a prueba, ofreciendo así confianza en su correción, e incluye técnicas tales como la verificadora de modelos a través de la exploración del espacio de estados y técnicas probadoras de teoremas automatizados. El más automatizado y sin lugar a duda la más popular técnica de verificación formal es la verificadora de modelos simbólica. Mientras obtiene éxito como un método valioso para la verificación de los diseños comerciales secuenciales, todavía es limitado con relación al tamaño de los diseños verificables. Actualmente existe una brecha real de verificación en diseños muy grandes que pueden ser fabricados pero no verificados debido a la complejidad de los problemas. El sector académico y grandes empresas industriales y gubernamentales se enfrentan a grandes retos para reducir la brecha tecnológica, proponiendo nuevas e ingeniosas soluciones en la especificación, creación de los casos de prueba y verificación.