En informática , los métodos formales son técnicas matemáticamente rigurosas para la especificación , desarrollo, análisis y verificación de sistemas de software y hardware . [1] El uso de métodos formales para el diseño de software y hardware está motivado por la expectativa de que, como en otras disciplinas de ingeniería, realizar un análisis matemático apropiado puede contribuir a la confiabilidad y solidez de un diseño. [2]
Los métodos formales emplean una variedad de fundamentos teóricos de la ciencia informática , incluidos cálculos lógicos , lenguajes formales , teoría de autómatas , teoría de control , semántica de programas , sistemas de tipos y teoría de tipos . [3]
Los métodos formales se pueden aplicar en varios puntos del proceso de desarrollo .
Se pueden utilizar métodos formales para dar una descripción formal del sistema que se va a desarrollar, con el nivel de detalle que se desee. Otros métodos formales pueden depender de esta especificación para sintetizar un programa o verificar la corrección de un sistema.
Alternativamente, la especificación puede ser la única etapa en la que se utilizan métodos formales. Al escribir una especificación, se pueden descubrir y resolver ambigüedades en los requisitos informales. Además, los ingenieros pueden usar una especificación formal como referencia para guiar sus procesos de desarrollo. [4]
La necesidad de sistemas de especificación formales se ha señalado durante años. En el informe ALGOL 58 , [5] John Backus presentó una notación formal para describir la sintaxis de los lenguajes de programación , posteriormente denominada forma normal de Backus y luego rebautizada como forma Backus–Naur (BNF). [6] Backus también escribió que no se completó a tiempo una descripción formal del significado de los programas ALGOL sintácticamente válidos para su inclusión en el informe, afirmando que "se incluirá en un artículo posterior". Sin embargo, nunca se publicó ningún artículo que describiera la semántica formal. [7]
La síntesis de programas es el proceso de creación automática de un programa que se ajusta a una especificación. Los métodos de síntesis deductivos se basan en una especificación formal completa del programa, mientras que los métodos inductivos infieren la especificación a partir de ejemplos. Los sintetizadores realizan una búsqueda en el espacio de posibles programas para encontrar un programa que sea coherente con la especificación. Debido al tamaño de este espacio de búsqueda, el desarrollo de algoritmos de búsqueda eficientes es uno de los principales desafíos en la síntesis de programas. [8]
La verificación formal es el uso de herramientas de software para probar las propiedades de una especificación formal o para probar que un modelo formal de una implementación de sistema satisface su especificación.
Una vez que se ha desarrollado una especificación formal, ésta puede utilizarse como base para probar las propiedades de la especificación y, por inferencia, las propiedades de la implementación del sistema.
La verificación de aprobación es el uso de una herramienta de verificación formal que goza de gran confianza. Dicha herramienta puede reemplazar a los métodos de verificación tradicionales (la herramienta puede incluso estar certificada). [ cita requerida ]
A veces, la motivación para demostrar la corrección de un sistema no es la necesidad obvia de reafirmar la corrección del sistema, sino el deseo de comprenderlo mejor. En consecuencia, algunas pruebas de corrección se producen al estilo de las pruebas matemáticas : escritas a mano (o tipográficas) utilizando lenguaje natural , utilizando un nivel de informalidad común a tales pruebas. Una prueba "buena" es aquella que es legible y comprensible para otros lectores humanos.
Los críticos de estos enfoques señalan que la ambigüedad inherente al lenguaje natural permite que no se detecten errores en dichas demostraciones; a menudo, pueden estar presentes errores sutiles en los detalles de bajo nivel que normalmente se pasan por alto en dichas demostraciones. Además, el trabajo que implica producir una demostración tan buena requiere un alto nivel de sofisticación y experiencia matemática.
En cambio, existe un creciente interés en producir pruebas de la corrección de dichos sistemas por medios automatizados. Las técnicas automatizadas se dividen en tres categorías generales:
Algunos probadores de teoremas automáticos requieren una guía para determinar qué propiedades son lo suficientemente "interesantes" como para investigarlas, mientras que otros funcionan sin intervención humana. Los verificadores de modelos pueden atascarse rápidamente en la comprobación de millones de estados poco interesantes si no se les proporciona un modelo suficientemente abstracto.
Los defensores de estos sistemas sostienen que los resultados tienen una mayor certeza matemática que las pruebas producidas por humanos, ya que todos los tediosos detalles han sido verificados algorítmicamente. El entrenamiento necesario para utilizar estos sistemas también es menor que el que se requiere para producir buenas pruebas matemáticas a mano, lo que hace que las técnicas sean accesibles a una variedad más amplia de profesionales.
Los críticos señalan que algunos de esos sistemas son como oráculos : hacen un pronunciamiento sobre la verdad, pero no dan ninguna explicación de esa verdad. También está el problema de " verificar al verificador ": si el programa que ayuda en la verificación no está probado, puede haber razones para dudar de la solidez de los resultados obtenidos. Algunas herramientas modernas de verificación de modelos producen un "registro de pruebas" que detalla cada paso de su prueba, lo que hace posible realizar, si se utilizan las herramientas adecuadas, una verificación independiente.
La característica principal del enfoque de interpretación abstracta es que proporciona un análisis sólido, es decir, no se obtienen falsos negativos. Además, es eficientemente escalable, al ajustar el dominio abstracto que representa la propiedad que se va a analizar y al aplicar operadores de ampliación [9] para obtener una convergencia rápida.
Los métodos formales incluyen una serie de técnicas diferentes.
El diseño de un sistema informático se puede expresar mediante un lenguaje de especificación, que es un lenguaje formal que incluye un sistema de pruebas. Mediante este sistema de pruebas, las herramientas de verificación formal pueden razonar sobre la especificación y establecer que un sistema se adhiere a ella. [10]
Un diagrama de decisión binario es una estructura de datos que representa una función booleana . [11] Si una fórmula booleana expresa que una ejecución de un programa se ajusta a la especificación, se puede utilizar un diagrama de decisión binario para determinar si es una tautología; es decir, siempre se evalúa como VERDADERO. Si este es el caso, entonces el programa siempre se ajusta a la especificación. [12]
Un solucionador SAT es un programa que puede resolver el problema de satisfacibilidad booleano , el problema de encontrar una asignación de variables que haga que una fórmula proposicional dada evalúe como verdadera. Si una fórmula booleana expresa que una ejecución específica de un programa se ajusta a la especificación, entonces determinar que es insatisfacible es equivalente a determinar que todas las ejecuciones se ajustan a la especificación. Los solucionadores SAT se utilizan a menudo en la verificación de modelos acotados, pero también se pueden utilizar en la verificación de modelos no acotados. [13]
Los métodos formales se aplican en diferentes áreas de hardware y software, incluidos enrutadores , conmutadores Ethernet , protocolos de enrutamiento , aplicaciones de seguridad y microkernels de sistemas operativos como seL4 . Hay varios ejemplos en los que se han utilizado para verificar la funcionalidad del hardware y software utilizados en centros de datos . IBM utilizó ACL2 , un demostrador de teoremas, en el proceso de desarrollo del procesador AMD x86. [ cita requerida ] Intel utiliza dichos métodos para verificar su hardware y firmware (software permanente programado en una memoria de solo lectura ) [ cita requerida ] . Dansk Datamatik Center utilizó métodos formales en la década de 1980 para desarrollar un sistema de compilación para el lenguaje de programación Ada que se convirtió en un producto comercial de larga duración. [ 14 ] [ 15 ]
Existen otros proyectos de la NASA en los que se aplican métodos formales, como Next Generation Air Transportation System [ cita requerida ] , Unmanned Aircraft System integration in National Airspace System, [16] y Airborne Coordinated Conflict Resolution and Detection (ACCoRD). [17] B-Method con Atelier B , [18] se utiliza para desarrollar automatismos de seguridad para los distintos metros instalados en todo el mundo por Alstom y Siemens , y también para la certificación Common Criteria y el desarrollo de modelos de sistemas por ATMEL y STMicroelectronics .
La verificación formal ha sido utilizada frecuentemente en hardware por la mayoría de los proveedores de hardware conocidos, como IBM, Intel y AMD. Hay muchas áreas de hardware, donde Intel ha utilizado métodos formales para verificar el funcionamiento de los productos, como la verificación parametrizada del protocolo coherente con la caché, [19] la validación del motor de ejecución del procesador Intel Core i7 [20] (usando la demostración de teoremas, BDD y evaluación simbólica), la optimización para la arquitectura Intel IA-64 usando el demostrador de teoremas de luz HOL, [21] y la verificación del controlador Gigabit Ethernet de doble puerto de alto rendimiento con soporte para el protocolo PCI Express y la tecnología de gestión avanzada de Intel usando Cadence. [22] De manera similar, IBM ha utilizado métodos formales en la verificación de puertas de energía, [23] registros, [24] y la verificación funcional del microprocesador IBM Power7. [25]
En el desarrollo de software , los métodos formales son enfoques matemáticos para resolver problemas de software (y hardware) en los niveles de requisitos, especificación y diseño. Es más probable que los métodos formales se apliquen a software y sistemas críticos para la seguridad o la protección, como el software de aviónica . Los estándares de garantía de seguridad del software, como DO-178C, permiten el uso de métodos formales a través de complementos, y Common Criteria exige el uso de métodos formales en los niveles más altos de categorización.
Para el software secuencial, los ejemplos de métodos formales incluyen el método B , los lenguajes de especificación utilizados en la demostración automática de teoremas , RAISE y la notación Z.
En programación funcional , las pruebas basadas en propiedades han permitido la especificación matemática y la prueba (si no una prueba exhaustiva) del comportamiento esperado de funciones individuales.
El lenguaje de restricción de objetos (y especializaciones como el lenguaje de modelado Java ) ha permitido que los sistemas orientados a objetos se especifiquen formalmente, si bien no necesariamente se verifiquen formalmente.
Para el software y los sistemas concurrentes, las redes de Petri , el álgebra de procesos y las máquinas de estados finitos (que se basan en la teoría de autómatas ; consulte también máquina de estados finitos virtual o máquina de estados finitos impulsada por eventos ) permiten la especificación de software ejecutable y pueden usarse para construir y validar el comportamiento de la aplicación.
Otro enfoque de los métodos formales en el desarrollo de software consiste en escribir una especificación en alguna forma de lógica (normalmente una variación de la lógica de primer orden ) y luego ejecutar directamente la lógica como si fuera un programa. El lenguaje OWL , basado en la lógica de descripción , es un ejemplo. También se trabaja en la asignación automática de alguna versión del inglés (u otro lenguaje natural) a la lógica y desde ella, así como en la ejecución directa de la lógica. Algunos ejemplos son Attempto Controlled English e Internet Business Logic, que no buscan controlar el vocabulario ni la sintaxis. Una característica de los sistemas que admiten la asignación bidireccional de la lógica al inglés y la ejecución directa de la lógica es que se puede hacer que expliquen sus resultados, en inglés, a nivel empresarial o científico. [ cita requerida ]
Los métodos semiformales son formalismos y lenguajes que no se consideran completamente "formales". Dejan la tarea de completar la semántica para una etapa posterior, que luego se realiza mediante interpretación humana o mediante software como generadores de código o casos de prueba . [26]
Algunos profesionales creen que la comunidad de métodos formales ha puesto demasiado énfasis en la formalización completa de una especificación o diseño. [27] [28] Sostienen que la expresividad de los lenguajes involucrados, así como la complejidad de los sistemas que se modelan, hacen que la formalización completa sea una tarea difícil y costosa. Como alternativa, se han propuesto varios métodos formales ligeros , que enfatizan la especificación parcial y la aplicación enfocada. Ejemplos de este enfoque ligero para los métodos formales incluyen la notación de modelado de objetos Alloy , [29] la síntesis de Denney de algunos aspectos de la notación Z con desarrollo impulsado por casos de uso , [30] y las herramientas CSK VDM . [31]
Hay una variedad de métodos formales y notaciones disponibles.
Muchos problemas en los métodos formales son NP-hard , pero pueden resolverse en casos que surgen en la práctica. Por ejemplo, el problema de satisfacibilidad booleano es NP-completo según el teorema de Cook-Levin , pero los solucionadores SAT pueden resolver una variedad de instancias grandes. Hay "solucionadores" para una variedad de problemas que surgen en los métodos formales, y hay muchas competiciones periódicas para evaluar el estado del arte en la solución de tales problemas. [33]
{{cite journal}}: Requiere citar revista |journal=( ayuda )