En informática , las especificaciones formales son técnicas basadas en matemáticas cuyo propósito es ayudar con la implementación de sistemas y software. Se utilizan para describir un sistema, analizar su comportamiento y ayudar en su diseño verificando propiedades clave de interés mediante herramientas de razonamiento rigurosas y efectivas. [1] [2] Estas especificaciones son formales en el sentido de que tienen una sintaxis, su semántica cae dentro de un dominio y se pueden usar para inferir información útil. [3]
En cada década que pasa, los sistemas informáticos se han vuelto cada vez más potentes y, como resultado, han tenido un mayor impacto en la sociedad. Debido a esto, se necesitan mejores técnicas para ayudar en el diseño e implementación de software confiable. Las disciplinas de ingeniería establecidas utilizan el análisis matemático como base para crear y validar el diseño de productos. Las especificaciones formales son una de esas formas de lograr esto en la ingeniería de software, ya que la confiabilidad se predijo anteriormente. Otros métodos, como las pruebas, se utilizan con más frecuencia para mejorar la calidad del código. [1]
Dada una especificación de este tipo , es posible utilizar técnicas de verificación formal para demostrar que el diseño de un sistema es correcto con respecto a su especificación. Esto permite revisar los diseños de sistemas incorrectos antes de que se hayan realizado inversiones importantes en una implementación real. Otro enfoque es utilizar pasos de refinamiento probablemente correctos para transformar una especificación en un diseño, que finalmente se transforma en una implementación que es correcta por construcción .
Es importante tener en cuenta que una especificación formal no es una implementación, sino que puede utilizarse para desarrollar una implementación . Las especificaciones formales describen lo que un sistema debería hacer, no cómo debería hacerlo.
Una buena especificación debe tener algunos de los siguientes atributos: adecuada, internamente consistente, inequívoca, completa, satisfecha y mínima. [3]
Una buena especificación tendrá: [3]
Una de las principales razones por las que existe interés en las especificaciones formales es que proporcionarán la capacidad de realizar pruebas en las implementaciones de software. [2] Estas pruebas se pueden utilizar para validar una especificación, verificar la corrección del diseño o demostrar que un programa satisface una especificación. [2]
Un diseño (o implementación) nunca puede ser declarado “correcto” por sí solo. Solo puede ser “correcto con respecto a una especificación dada”. Si la especificación formal describe correctamente el problema a resolver es una cuestión aparte. También es una cuestión difícil de abordar ya que en última instancia concierne al problema de construir representaciones formales abstractas de un dominio de problema concreto informal , y tal paso de abstracción no es susceptible de prueba formal. Sin embargo, es posible validar una especificación probando teoremas de “desafío” relacionados con las propiedades que se espera que presente la especificación. Si son correctos, estos teoremas refuerzan la comprensión del especificador de la especificación y su relación con el dominio del problema subyacente. Si no, la especificación probablemente deba modificarse para reflejar mejor la comprensión del dominio de quienes participan en la producción (e implementación) de la especificación.
Los métodos formales de desarrollo de software no se utilizan ampliamente en la industria. La mayoría de las empresas no consideran rentable aplicarlos en sus procesos de desarrollo de software. [4] Esto puede deberse a diversas razones, algunas de las cuales son:
Otras limitaciones: [3]
Las técnicas de especificación formal existen desde hace mucho tiempo en diversos dominios y a distintas escalas. [6] Las implementaciones de especificaciones formales variarán según el tipo de sistema que se intente modelar, cómo se apliquen y en qué punto del ciclo de vida del software se hayan introducido. [2] Estos tipos de modelos se pueden clasificar en los siguientes paradigmas de especificación:
Además de los paradigmas anteriores, existen formas de aplicar ciertas heurísticas para ayudar a mejorar la creación de estas especificaciones. El artículo al que se hace referencia aquí analiza mejor las heurísticas que se deben utilizar al diseñar una especificación. [6] Lo hacen aplicando un enfoque de divide y vencerás .
La notación Z es un ejemplo de un lenguaje de especificación formal líder . Otros incluyen el lenguaje de especificación (VDM-SL) del método de desarrollo de Viena y la notación de máquina abstracta (AMN) del método B. En el área de servicios web , la especificación formal se utiliza a menudo para describir propiedades no funcionales [7] ( calidad de servicio de servicios web ).
Algunas herramientas son: [4]
