Especificación formal
Aspecto de la informática

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]

Motivación

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]

Usos

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]

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

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]

Limitaciones

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:

  • Tiempo
    • Altos costos iniciales de puesta en marcha con bajos rendimientos mensurables
  • Flexibilidad
    • Muchas empresas de software utilizan metodologías ágiles que se centran en la flexibilidad. Realizar una especificación formal de todo el sistema por adelantado suele considerarse lo contrario de 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 habilidades analíticas para comprenderlos y aplicarlos de manera efectiva [5].
    • Una solución a esto sería desarrollar herramientas y modelos que permitan implementar estas técnicas pero que oculten las matemáticas subyacentes [2] [5]
  • Alcance limitado [3]
    • No capturan propiedades de interés para todos los interesados ​​en el proyecto [3]
    • No hacen un buen trabajo al especificar las interfaces de usuario y la interacción del usuario [4]
  • No es rentable
    • Esto no es del todo cierto, ya que al limitar su uso únicamente a partes centrales de sistemas críticos han demostrado ser rentables [4].

Otras limitaciones: [3]

Paradigmas

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:

  • Especificación basada en la historia [3]
    • comportamiento basado en historiales del sistema
    • Las afirmaciones se interpretan a lo largo del tiempo.
  • Especificación basada en estados [3]
    • comportamiento basado en 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 transición [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 primeros lenguajes como Paisley, GIST, redes de Petri o álgebras de procesos se basan en este paradigma [3]

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 .

Herramientas de software

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]

Véase también

Referencias

  1. ^ ab Hierons, RM; Bogdanov, K.; Bowen, JP ; Cleaveland, R.; Derrick, J.; Dick, J.; Gheorghe, M.; Harman, M .; Kapoor, K.; Krause, P.; Lüttgen, G.; Simons, AJH; Vilkomir, SA ; Woodward, MR; Zedan, H. (2009). "Uso de especificaciones formales para respaldar las pruebas". Encuestas de computación de ACM . 41 (2): 1. CiteSeerX  10.1.1.144.3320 . doi :10.1145/1459352.1459354. S2CID  10686134.
  2. ^ abcde Gaudel, M.-C. (1994). "Técnicas de especificación formal". Actas de la 16.ª Conferencia internacional sobre ingeniería de software . págs. 223-227. doi :10.1109/ICSE.1994.296781. ISBN 978-0-8186-5855-6.S2CID60740848  .​
  3. ^ abcdefghijklmno Lamsweerde, AV (2000). "Especificación formal". Actas de la conferencia sobre el futuro de la ingeniería de software - ICSE '00 . págs. 147–159. doi :10.1145/336512.336546. ISBN 978-1581132533.S2CID 4657483  .
  4. ^ abcd Sommerville, Ian (2009). "Especificación formal" (PDF) . Ingeniería de software . Consultado el 3 de febrero de 2013 .
  5. ^ abcNummenmaa, Timo; Tiensuu, Aleksi; Berki, Eleni; Mikkonen, Tommi; Kuittinen, Jussi; Kultima, Annakaisa (4 de agosto de 2011). "Apoyar el desarrollo ágil facilitando la interacción natural del usuario con especificaciones formales ejecutables". Notas de ingeniería de software de ACM SIGSOFT . 36 (4): 1–10. doi :10.1145/1988997.2003643. S2CID  2139235.
  6. ^ ab van der Poll, John A.; Paula Kotze (2002). "¿Qué heurísticas de diseño pueden mejorar la utilidad de una especificación formal?". Actas de la Conferencia Anual de Investigación de 2002 del Instituto Sudafricano de Científicos Informáticos y Tecnólogos de la Información sobre Habilitación a través de la Tecnología . SAICSIT '02: 179–194. ISBN 9781581135961.
  7. ^ Modelo de conocimiento S-Cube: especificación formal
Wikimedia Commons tiene medios relacionados con Especificación formal .
  • Un caso a favor de la especificación formal (Tecnología) Archivado el 21 de octubre de 2005 en Wayback Machine por Coryoth 2005-07-30
Obtenido de "https://es.wikipedia.org/w/index.php?title=Especificación_formal&oldid=1225782806"