En informática e ingeniería del software, los métodos formales son un grupo de técnicas basadas en un aparato matemático para la especificación , desarrollo y verificación de software y hardware [1] . El uso de métodos formales para el diseño de software y hardware se debe a la expectativa de que, como en otros campos de la ingeniería, el uso del análisis matemático puede aumentar significativamente la confiabilidad de los sistemas [2] . Al mismo tiempo, los métodos formales son bastante complejos, requieren capacitación especial, inversiones en tiempo y recursos y, a menudo, se basan en suposiciones que no siempre se pueden lograr en condiciones reales. Esto lleva al hecho de que los métodos formales se utilizan con mayor frecuencia en el diseño de sistemas de alta precisión, donde la importancia de la seguridad justifica cualquier medio.
Los métodos formales se ocupan de la aplicación de una clase bastante amplia de técnicas fundamentales de la informática teórica : varios cálculos de lógica , lenguajes formales , teoría de autómatas , semántica formal , sistemas de tipos y tipos de datos algebraicos [3] .
Hay tres niveles de aplicación de los métodos formales:
Nivel cero Se desarrolla una especificación formal , luego se escribe el código del programa viéndolo . En este caso, la brecha entre la parte formal e informal sigue sin demostrarse, pero la solución puede ser rentable. Primer nivel El código del programa se deriva automáticamente de la especificación formal , se utilizan mecanismos de verificación y se prueban las propiedades más críticas del sistema. Este camino se elige a menudo para sistemas de alta precisión. Segundo nivel Los probadores automáticos de teoremas se utilizan para derivar pruebas completamente formalizadas que se verifican automáticamente. El enfoque requiere mucha inversión e investigación, pero vale la pena en las partes más críticas de los sistemas complejos donde no se permiten errores (por ejemplo, en el diseño de circuitos integrados ).Los enfoques de métodos formales también se pueden clasificar de manera similar a la semántica formal de los lenguajes de programación :
Semántica denotacional _ _ _ El significado de un sistema se expresa en términos de conjuntos parcialmente ordenados , y los métodos se basan en una teoría bien desarrollada en torno a ellos. La limitación del método es que no todos los sistemas pueden ser considerados intuitiva o naturalmente como una función . Semántica operacional _ _ _ El valor de un sistema se denota mediante una secuencia de acciones dentro de un modelo computacional más simple (como el cálculo lambda o las redes de Petri ). Los métodos son notorios por su simplicidad, si no enfatizados en el hecho de que se basan en la semántica de un sistema “más simple”, que también necesita ser definido a través de algo. Semántica axiomática _ _ _ El significado del sistema se define en términos de precondiciones y poscondiciones , lo que permite conectar la teoría con la lógica clásica, pero no da una idea de qué sucede exactamente dentro del sistema (cómo se logran las poscondiciones en base a las precondiciones) .Además, a menudo se pueden lograr resultados dramáticamente positivos sacrificando la aplicabilidad global y la formalización excesiva; estos casos se denominan métodos formales "ligeros" (lightweight). Se pueden dividir en dos tipos: con automatización mejorada y con automatización debilitada. Un ejemplo de automatización mejorada es el analizador de especificaciones Alloy Analyzer , que, para reducir el problema de encontrar un modelo a uno solucionable, reduce el área de búsqueda (como resultado, Alloy funciona completamente automatizado, a diferencia de los probadores interactivos, pero tiene un posibilidad de no encontrar algunos problemas). Un ejemplo de uno debilitado es la convergencia de gramáticas , en la que la irresolubilidad del problema de equivalencia de dos lenguajes formales se maneja por el hecho de que las transformaciones las realiza la propia persona, y las conclusiones ya se extraen de las propiedades. de los operadores utilizados por él.
Los métodos formales se aplican en diferentes etapas del desarrollo de software :
Especificación Con la ayuda de métodos formales, es posible describir el futuro sistema con cualquier nivel de detalle. Tal descripción formal se puede utilizar directa o indirectamente en beneficio de etapas posteriores. Al mismo tiempo, el trabajo para probar una serie de propiedades funcionales requeridas puede comenzar de inmediato e ir en paralelo con la escritura o generación de código. Hay varios lenguajes y cálculos para las especificaciones formales, pero ninguno puede pretender ser tan universal como la forma Backus-Naur para la especificación sintáctica . Desarrollo Si una especificación formal usa semántica operativa, el comportamiento observado de un sistema en particular puede compararse con el comportamiento esperado, porque tal semántica puede ser factible e incluso puede usarse para la generación automática de código. Si se utiliza la semántica axiomática, las condiciones previas y posteriores pueden asignarse directamente a declaraciones en código ejecutable. Verificación Una vez que se ha preparado una especificación formal, se puede utilizar para probar las propiedades requeridas. La verificación puede ser deductiva y modelo : la deductiva utiliza la prueba automática de teoremas o álgebras específicas , y el modelo basa sus conclusiones no en el sistema mismo, sino en el modelo construido sobre él [4] . Al mismo tiempo, no es absolutamente necesario construir el modelo manualmente, si son aplicables técnicas como la sección de programa .Las pruebas manuales requieren una importante inversión de recursos y no proporcionan ningún beneficio más que la confirmación de la corrección. Como resultado, los métodos formales se utilizan en áreas donde la evidencia puede obtenerse automáticamente mediante software o en aquellas donde el costo del error es demasiado alto (por ejemplo, al crear naves espaciales o imágenes de resonancia magnética ).
| Desarrollo de software | |
|---|---|
| Proceso | |
Conceptos de alto nivel | |
| Direcciones |
|
| Metodologías de desarrollo | |
| Modelos |
|
Figuras notables |
|