En informática , las especificaciones formales son técnicas de base matemática 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 a través de 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 pueden usarse para inferir información útil. [3]
En cada década que pasa, los sistemas informáticos se han vuelto cada vez más poderosos y, como resultado, han adquirido 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 la creación y validación del diseño de productos. Las especificaciones formales son una de esas formas de lograr esto en la confiabilidad de la ingeniería de software como alguna vez se predijo. Otros métodos, como las pruebas, se utilizan más comúnmente para mejorar la calidad del código. [1]
Dada tal especificación , 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 incorrectos del sistema antes de realizar 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 en última instancia se transforma en una implementación correcta por construcción .
Es importante señalar que una especificación formal no es una implementación, sino que puede usarse para desarrollar una implementación . Las especificaciones formales describen lo que debe hacer un sistema, no cómo debe hacerlo.
Una buena especificación debe tener algunos de los siguientes atributos: adecuada, internamente consistente, inequívoca, completa, satisfactoria 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 brindarán la capacidad de realizar pruebas en implementaciones de software. [2] Estas pruebas pueden usarse para validar una especificación, verificar la corrección del diseño o para demostrar que un programa satisface una especificación. [2]
Un diseño (o implementación) nunca puede declararse “correcto” por sí solo. Sólo puede ser "correcto con respecto a una especificación determinada". Si la especificación formal describe correctamente el problema a resolver es un tema aparte. También es una cuestión difícil de abordar, ya que en última instancia se refiere 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 demostrando teoremas de "desafío" relacionados con las propiedades que se espera que exhiba la especificación. Si son correctos, estos teoremas refuerzan la comprensión de la especificación por parte del especificador y su relación con el dominio del problema subyacente. De lo contrario, probablemente sea necesario cambiar la especificación para reflejar mejor la comprensión del dominio por parte 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 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 han existido en diversos dominios y en diversas escalas desde hace bastante tiempo. [6] Las implementaciones de especificaciones formales diferirán según el tipo de sistema que se intente modelar, cómo se aplican y en qué punto del ciclo de vida del software se han 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]
