La especificación formal en contexto: actual y futuro

Formal specification in context: current and future

La especificación formal es un área de investigación activa en la ingeniería de software de este siglo, enla que se aplica en diversas configuraciones y técnicas, y aunque su uso industrial todavía es limitado,la comunidad científica tiene actualmente una comprensión diferente acerca de su utilidad y necesidad.Hasta el momento el trabajo de los investigadores se focaliza en la especificación escrita durante eldiseño del modelo funcional preliminar, por lo que se centra principalmente en evaluar las herramientasrelacionadas. En este trabajo se realiza una revisión a la literatura, se hace un recorrido por la esencia,la función, el uso y los inconvenientes de las técnicas de especificación formal y se analizan algunoscriterios de valoración y de evaluación a sus debilidades. Los resultados se convierten en la base paraformular trabajos futuros, con el objetivo de buscar que la especificación formal se afiance como actividadbásica de investigación.

INTRODUCCIÓN

Desde el surgimiento de las Ciencias Computacionales los investigadores han considerado a la especificación formal (FS por sus siglas en inglés) como una de sus áreas de interés. Finalizando los años cuarenta Turing [1] observó que el razonamiento acerca de programas secuenciales era más sencillo cuando, en puntos específicos del mismo, se hacían anotaciones acerca de las propiedades de su estado. En los años sesenta Floyd [2], Hoare [3] y Naur [4] propusieron técnicas axiomáticas para demostrar la consistencia entre los programas secuenciales y esas propiedades, a las que llamaron especificaciones, y Dijkstra [5] demostró cómo utilizar constructivamente el cálculo para derivar programas no determinísticos que las cumplieran. Parnas [6] y Liskov [7] propusieron técnicas específicas para expresar formalmente las propiedades de los programas, particularmente para datos estructurados, y Pnueli [8] lo hizo para programas concurrentes. Estos aportes conformaron el punto de partida para la especificación formal como una nueva área de investigación [9, 11], y desde entonces se ha incrementado continuamente el interés que despertó, lo mismo que los múltiples usos en la ingeniería de software [12-14]. Hasta el momento el objetivo principal de esta comunidad de investigadores se focaliza en la especificación escrita durante el diseño del modelo funcional preliminar [12], por lo que su investigación, alrededor de la cual se genera este trabajo, se centra principalmente en evaluar y comparar las herramientas relacionadas con esta especificación y en analizar sus fortalezas y debilidades.

En este artículo se presenta el resultado de una revisión a la literatura para determinar la esencia, la función, el uso y los inconvenientes de las técnicas de especificación formal. Se discuten algunos criterios de valoración y se hace una evaluación a sus fortalezas y debilidades.