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 mediante la verificación de 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]
Motivación
En cada década que pasa, los sistemas informáticos se han vuelto cada vez más poderosos y, como resultado, se han vuelto más impactantes para 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 las formas de lograr esto en la confiabilidad de la ingeniería de software como se predijo. Otros métodos, como las pruebas, se utilizan con más frecuencia para mejorar la calidad del código. [1]
Usos
Dada tal especificación , es posible utilizar técnicas de verificación formales para demostrar que el diseño de un sistema es correcto con respecto a su especificación. Esto permite que se revisen 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 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 debería hacer un sistema, no cómo debería 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]
- Constructabilidad, 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 implementaciones de software. [2] Estas pruebas pueden usarse para validar una especificación, verificar la corrección del diseño o para probar 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 un tema aparte. También es un tema difícil de abordar, ya que en última instancia se refiere al problema de la construcción de 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" con respecto a las propiedades que se espera que muestre la especificación. Si es correcto, estos teoremas refuerzan la comprensión del especificador de la especificación y su relación con el dominio del problema subyacente. De lo contrario, la especificación probablemente deba cambiarse para reflejar mejor la comprensión del dominio de aquellos involucrados 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 una variedad de razones, algunas de las cuales son:
- Hora
- Alto costo inicial de puesta en marcha con bajos rendimientos medibles
- Flexibilidad
- Muchas empresas de software utilizan metodologías ágiles que se centran en la flexibilidad. Hacer una especificación formal de todo el sistema por adelantado a menudo se percibe como lo opuesto a lo flexible. Sin embargo, hay algunas investigaciones sobre los beneficios de utilizar especificaciones formales con un desarrollo "ágil" [5].
- Complejidad
- 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 rentable
- Esto no es del todo cierto, al limitar su uso solo a las partes centrales de los sistemas críticos que han demostrado ser rentables [4].
Otras limitaciones: [3]
- Aislamiento
- Ontologías de bajo nivel
- Mala orientación
- Mala separación de preocupaciones
- Comentarios deficientes sobre la herramienta
Paradigmas
Las técnicas de especificación formal han existido en varios dominios y en varias escalas durante bastante tiempo. [6] Las implementaciones de especificaciones formales diferirán según el tipo de sistema que intenten 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 el historial [3]
- comportamiento basado en historias del sistema
- las afirmaciones se interpretan a lo largo del tiempo
- Especificación basada en el estado [3]
- Especificación basada en la transición [3]
- comportamiento basado en transiciones de un estado a otro del sistema
- mejor utilizado 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, hay formas de aplicar ciertas heurísticas para ayudar a mejorar la creación de estas especificaciones. El documento al que se hace referencia aquí analiza mejor la heurística que se debe 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 la especificación del lenguaje (VDM-SL) del método de desarrollo de Viena y de la máquina abstracta de notación (AMN) de la B-Método . En el área de 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
- Alerce
- OBJ
- Loto
- Basado en modelos
- Z
- B
- VDM
- CSP
- Redes de Petri
- TLA +
- Basado en navegación y gráficos de contenido:
- Figma
Ejemplos de
Para ver ejemplos de implementación, consulte los enlaces en la sección de herramientas de software .
Ver también
- Especificación algebraica
- Métodos formales
- Especificación basada en modelos
- Ingeniería de software
- Lenguaje de especificación
- Especificación (estándar técnico)
Referencias
- ^ a b Hierones, 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 ACM . 41 (2): 1. CiteSeerX 10.1.1.144.3320 . doi : 10.1145 / 1459352.1459354 . S2CID 10686134 .
- ^ a b c d e Gaudel, M.-C. (1994). "Técnicas de especificación formal". Actas de la 16ª Conferencia Internacional de Ingeniería de Software . págs. 223–227. doi : 10.1109 / ICSE.1994.296781 . ISBN 978-0-8186-5855-6. S2CID 60740848 .
- ^ a b c d e f g h i j k l m n o 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 .
- ^ a b c d Sommerville, Ian (2009). "Especificación formal" (PDF) . Ingeniería de software . Consultado el 3 de febrero de 2013 .
- ^ a b c Nummenmaa, 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 del software ACM SIGSOFT . 36 (4): 1–10. doi : 10.1145 / 1988997.2003643 . S2CID 2139235 .
- ^ a b 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 en Computación y Tecnólogos de la Información sobre Habilitación a través de la Tecnología . SAICSIT '02: 179-194.
- ^ Modelo de conocimiento de S-Cube: especificación formal
enlaces externos
- Un caso para la especificación formal (tecnología) por Coryoth 2005-07-30
- Especificación formal