Bounded Verification of Software Models: Challenges and Opportunities

Resumen

Asegurar la ausencia de errores en un sistema software es un problema importante pero también un desafío. La detección temprana de errores en el proceso de desarrollo de software reduce el coste de detectar y corregir los defectos. Así pues, el análisis de modelos puede incrementar la calidad final del software y reducir los costes de desarrollo.

Una línea de investigación prometedora en este campo es el uso de solvers de satisfactibilidad booleana (SAT) o programación con restricciones (CP) para realizar verificación acotada. La verificación acotada consiste en comprovar formalmente la ausencia de errores dentro de un espacio finito definido como parámetro del análisis. Este tipo de análisis es usualmente rápido en la práctica y proporciona un feedback valioso. Sin embargo, su complejidad computacional es elevada en general y no ofrece resultados concluyentes fuera del rango de verificación definido como parámetro.

En este artículo, discutimos tendencias recientes y resultados en la aplicación de verificación acotada a un campo específico dentro de la ingeniería del software : el análisis de modelos de un sistema software. Además, discutimos contribuciones prometedoras que pueden ampliar el trabajo previo para mejorar su aplicabilidad práctica dentro de la industria del software.