Especificación formal

En informática , las especificaciones formales son técnicas basadas en las matemáticas cuyo propósito es facilitar la implementación de sistemas y software. Se utilizan para describir un sistema, analizar su comportamiento y contribuir a su diseño mediante la verificación de propiedades clave de interés a través de herramientas de razonamiento rigurosas y eficaces. ^{[ 1 ] [ 2 ]} Estas especificaciones son formales en el sentido de que poseen una sintaxis, su semántica se enmarca dentro de un dominio y permiten 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, su impacto en la sociedad ha aumentado. Por ello, se necesitan mejores técnicas para el diseño e implementación de software fiable. 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 forma de lograr la fiabilidad en la ingeniería de software, tal como se predijo. Otros métodos, como las pruebas, se utilizan con mayor frecuencia para mejorar la calidad del código. ^{[ 1 ]}

Con dicha especificación , es posible utilizar técnicas de verificación formal para demostrar que el diseño del sistema es correcto con respecto a dicha especificación. Esto permite revisar diseños de sistemas incorrectos antes de realizar inversiones importantes en su implementación. Otro enfoque consiste en utilizar pasos de refinamiento demostrablemente correctos para transformar una especificación en un diseño, que finalmente se transforma en una implementación correcta por construcción .

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 debe hacer, no cómo debe hacerlo.

Una buena especificación debe tener algunos de los siguientes atributos: adecuada, internamente consistente, inequívoca, completa, satisfecha, mínima. ^{[ 3 ]}

Una buena especificación tendrá: ^{[ 3 ]}

• Construibilidad, manejabilidad y capacidad de evolución.
• Usabilidad
• Comunicabilidad
• Análisis potente y eficiente

Una de las principales razones del interés en las especificaciones formales es que permiten realizar pruebas sobre las implementaciones de software. ^{[ 2 ]} Estas pruebas pueden utilizarse para validar una especificación, verificar la corrección del diseño o demostrar que un programa cumple con una especificación. ^{[ 2 ]}

Un diseño (o implementación) nunca puede declararse "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 se refiere al problema de construir representaciones formales abstractas de un dominio de problema concreto e informal , y tal paso de abstracción no se presta a una demostración formal. Sin embargo, es posible validar una especificación demostrando teoremas de "desafío" sobre las propiedades que se espera que presente la especificación. Si son correctos, estos teoremas refuerzan la comprensión que el especificador tiene de la especificación y su relación con el dominio del problema subyacente. De lo contrario, probablemente sea necesario modificar la especificación para que refleje mejor la comprensión del dominio por parte de quienes participan en su producción (e implementació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:

• Tiempo
  • Alto coste inicial de puesta en marcha con bajos retornos cuantificables.
• Flexibilidad
  • Muchas empresas de software utilizan metodologías ágiles que se centran en la flexibilidad. Realizar una especificación formal de todo el sistema desde el principio suele percibirse como lo opuesto a la flexibilidad. Sin embargo, existen algunas investigaciones sobre los beneficios de utilizar especificaciones formales con el desarrollo "ágil" ^{[ 5 ].}
• Complejidad
  • Requieren un alto nivel de conocimientos matemáticos y las habilidades analíticas para comprenderlos y aplicarlos eficazmente ^{[ 5 ].}
  • Una solución a esto sería desarrollar herramientas y modelos que permitan implementar estas técnicas pero oculten las matemáticas subyacentes ^{[ 2 ] [ 5 ].}
• Alcance limitado ^{[ 3 ]}
  • No capturan propiedades de interés para todas las partes interesadas en el proyecto ^{[ 3 ].}
  • No hacen un buen trabajo especificando las interfaces de usuario y la interacción del usuario ^{[ 4 ].}
• No es rentable
  • Esto no es del todo cierto; al limitar su uso solo a partes centrales de sistemas críticos, han demostrado ser rentables ^{[ 4 ].}

Otras limitaciones: ^{[ 3 ]}

• Aislamiento
• Ontologías de bajo nivel
• Mala orientación
• Mala separación de intereses
• Retroalimentación deficiente de la herramienta

Las técnicas de especificación formal han existido en diversos dominios y a diferentes escalas desde hace bastante tiempo. ^{[ 6 ]} Las implementaciones de especificaciones formales difieren según el tipo de sistema que intentan modelar, cómo se aplican y en qué punto del ciclo de vida del software se introducen. ^{[ 2 ]} Estos tipos de modelos se pueden clasificar en los siguientes paradigmas de especificación:

• Especificación basada en el historial ^{[ 3 ]}
  • comportamiento basado en historiales del sistema
  • Las afirmaciones se interpretan con el tiempo.
• Especificación basada en estados ^{[ 3 ]}
  • comportamiento basado en los estados del sistema
  • serie de pasos secuenciales, (por ejemplo, una transacción financiera)
  • Lenguajes como Z , VDM o B se basan en este paradigma ^{[ 3 ].}
• Especificación basada en transiciones ^{[ 3 ]}
  • comportamiento basado en transiciones de estado a estado del sistema
  • Se utiliza mejor con un sistema reactivo.
  • Lenguajes como Statecharts, PROMELA, STeP-SPL, RSML o SCR se basan en este paradigma ^{[ 3 ].}
• Especificación funcional ^{[ 3 ]}
  • especificar un sistema como una estructura de funciones matemáticas
  • OBJ, ASL, PLUSS, LARCH, HOL o PVS se basan en este paradigma ^{[ 3 ].}
• Especificación operativa ^{[ 3 ]}
  • Los lenguajes antiguos como Paisley , GIST, las redes de Petri o las álgebras de procesos se basan en este paradigma ^{[ 3 ].}
• Lenguas multiparadigmáticas
  • FizzBee es un lenguaje de especificación multiparadigma que permite la especificación basada en transiciones/acciones, especificaciones de comportamiento con transiciones no atómicas y también cuenta con un modelo de actores.

Además de los paradigmas mencionados, existen maneras de aplicar ciertas heurísticas para mejorar la creación de estas especificaciones. El artículo citado aquí analiza en detalle las heurísticas que se deben usar al diseñar una especificación. ^{[ 6 ]} Para ello, aplican un enfoque de divide y vencerás .

La notación Z es un ejemplo de un lenguaje de especificación formal líder . Otros ejemplos 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 ámbito de los servicios web , la especificación formal se utiliza a menudo para describir propiedades no funcionales ^{[ 7 ]} ( calidad de servicio de los servicios web ).

Algunas herramientas son: ^{[ 4 ]}

• Algebraico
  1. Alerce
  2. OBJ
  3. Loto
• Basado en modelos
  1. Z
  2. B
  3. VDM
  4. CSP
  5. Redes de Petri
  6. TLA+
  7. FizzBee

• Un argumento a favor de la especificación formal (tecnología) Archivado el 21/10/2005 en Wayback Machine por Coryoth el 30/07/2005