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 robustez de un diseño. [2]
Los métodos formales emplean una variedad de fundamentos teóricos de la 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 a desarrollar, con cualquier nivel de detalle deseado. 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 utilizar una especificación formal como referencia para guiar sus procesos de desarrollo. [4]
Durante años se ha observado la necesidad de sistemas de especificaciones formales. En el informe ALGOL 58 , [5] John Backus presentó una notación formal para describir la sintaxis del lenguaje de programación , más tarde denominada forma normal de Backus y luego rebautizada como forma Backus-Naur (BNF). [6] Backus también escribió que una descripción formal del significado de los programas ALGOL sintácticamente válidos no se completó a tiempo 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 crear automáticamente un programa que se ajuste a una especificación. Los enfoques de síntesis deductiva se basan en una especificación formal completa del programa, mientras que los enfoques 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 consistente con la especificación. Debido al tamaño de este espacio de búsqueda, desarrollar 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 propiedades de una especificación formal o para demostrar que un modelo formal de implementación de un sistema satisface su especificación.
Una vez que se ha desarrollado una especificación formal, la especificación puede usarse 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 es altamente confiable. Una herramienta de este tipo puede sustituir los métodos de verificación tradicionales (la herramienta puede incluso estar certificada). [ cita necesaria ]
A veces, la motivación para demostrar la corrección de un sistema no es la necesidad obvia de asegurarse de la corrección del sistema, sino el deseo de comprender mejor el sistema. En consecuencia, algunas pruebas de corrección se producen al estilo de la prueba matemática : escritas a mano (o tipografiadas) utilizando lenguaje natural , utilizando un nivel de informalidad común a tales pruebas. Una "buena" prueba es aquella que es legible y comprensible para otros lectores humanos.
Los críticos de tales enfoques señalan que la ambigüedad inherente al lenguaje natural permite que no se detecten errores en tales pruebas; A menudo, pueden estar presentes errores sutiles en los detalles de bajo nivel que normalmente pasan por alto tales pruebas. Además, el trabajo involucrado en producir una prueba tan buena requiere un alto nivel de sofisticación y experiencia matemática.
Por el contrario, existe un interés creciente en presentar pruebas de la exactitud de tales sistemas por medios automatizados. Las técnicas automatizadas se dividen en tres categorías generales:
Algunos demostradores de teoremas automatizados requieren orientación sobre qué propiedades son lo suficientemente "interesantes" como para seguirlas, mientras que otros funcionan sin intervención humana. Los verificadores de modelos pueden atascarse rápidamente en la verificación de millones de estados poco interesantes si no se les proporciona un modelo suficientemente abstracto.
Los defensores de tales sistemas argumentan que los resultados tienen mayor certeza matemática que las pruebas producidas por humanos, ya que todos los tediosos detalles han sido verificados algorítmicamente. La formación necesaria para utilizar dichos sistemas también es inferior a la necesaria para producir buenas demostraciones 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 de la verdad, pero no dan 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 motivos para dudar de la solidez de los resultados obtenidos. Algunas herramientas modernas de verificación de modelos producen un "registro de prueba" que detalla cada paso de su prueba, lo que permite realizar, con 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, que no arroja falsos negativos. Además, es escalable de manera eficiente, al ajustar el dominio abstracto que representa la propiedad a analizar y al aplicar operadores de ampliación [9] para lograr una convergencia rápida.
Los métodos formales incluyen varias técnicas diferentes.
El diseño de un sistema informático se puede expresar utilizando un lenguaje de especificación, que es un lenguaje formal que incluye un sistema de prueba. Al utilizar este sistema de prueba, las herramientas de verificación formal pueden razonar sobre la especificación y establecer que un sistema cumple con la especificación. [10]
Un diagrama de decisión binaria 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 se trata de una tautología; es decir, siempre se evalúa como VERDADERO. Si este es el caso, entonces el programa siempre se ajusta a las especificaciones. [12]
Un solucionador SAT es un programa que puede resolver el problema de satisfacibilidad booleana , el problema de encontrar una asignación de variables que haga que una fórmula proposicional dada se 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 insatisfactoria equivale a determinar que todas las ejecuciones se ajustan a la especificación. Los solucionadores SAT se utilizan a menudo en la comprobación de modelos acotados, pero también se pueden utilizar en la comprobación de modelos ilimitados. [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 . Existen varios ejemplos en los que se han utilizado para verificar la funcionalidad del hardware y software utilizado en los centros de datos . IBM utilizó ACL2 , un demostrador de teoremas, en el proceso de desarrollo del procesador AMD x86. [ cita necesaria ] Intel utiliza estos métodos para verificar su hardware y firmware (software permanente programado en una memoria de solo lectura ) [ cita necesaria ] . El Dansk Datamatik Center utilizó métodos formales en la década de 1980 para desarrollar un sistema compilador para el lenguaje de programación Ada que se convirtió en un producto comercial de larga duración. [14] [15]
Hay varios otros proyectos de la NASA en los que se aplican métodos formales, como el Sistema de transporte aéreo de próxima generación [ cita requerida ] , la integración del sistema de aeronaves no tripuladas en el Sistema Nacional del Espacio Aéreo, [16] y la Resolución y Detección Coordinada de Conflictos Aerotransportados (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 parte de ATMEL y STMicroelectronics .
La mayoría de los proveedores de hardware conocidos, como IBM, Intel y AMD, han utilizado con frecuencia la verificación formal en el hardware. Hay muchas áreas de hardware en las que Intel ha utilizado métodos formales para verificar el funcionamiento de los productos, como la verificación parametrizada del protocolo coherente de caché, [19] la validación del motor de ejecución del procesador Intel Core i7 [20] (mediante demostración de teoremas, BDD , y evaluación simbólica), optimización para la arquitectura Intel IA-64 utilizando el probador del teorema de la luz HOL, [21] y 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 utilizando Cadence. [22] De manera similar, IBM ha utilizado métodos formales en la verificación de puertas de alimentación, [23] registros, [24] y 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, especificaciones y diseño. Es más probable que los métodos formales se apliquen a software y sistemas críticos para la seguridad, 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 mediante complementación, y Common Criteria exige 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 automatizada 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 las pruebas (si no exhaustivas) del comportamiento esperado de funciones individuales.
El lenguaje de restricciones de objetos (y especializaciones como el lenguaje de modelado Java ) han permitido que los sistemas orientados a objetos se especifiquen formalmente, aunque no necesariamente se verifiquen formalmente.
Para software y 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 ; ver también máquina virtual de estados finitos o máquina de estados finitos impulsada por eventos ) permiten especificaciones de software ejecutables y pueden usarse para construir y validar. comportamiento de la aplicación.
Otro enfoque de los métodos formales en el desarrollo de software es escribir una especificación en alguna forma de lógica (generalmente 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 está trabajando en mapear alguna versión del inglés (u otro lenguaje natural) automáticamente hacia y desde la lógica, así como en ejecutar la lógica directamente. Ejemplos de ello 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 el mapeo bidireccional inglés-lógico y la ejecución directa de la lógica es que se les puede hacer explicar sus resultados, en inglés, a nivel empresarial o científico. [ cita necesaria ]
Los métodos semiformales son formalismos y lenguajes que no se consideran completamente "formales". Se difiere la tarea de completar la semántica para una etapa posterior, que luego se realiza mediante interpretación humana o mediante interpretación a través de software como código o generadores de casos de prueba . [26]
Algunos profesionales creen que la comunidad de métodos formales ha puesto demasiado énfasis en la formalización total 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 total 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 de 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-difíciles , pero pueden resolverse en los 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 casos grandes. Hay "solucionadores" para una variedad de problemas que surgen en los métodos formales, y hay muchos concursos periódicos para evaluar los últimos avances en la resolución de dichos problemas. [33]
{{cite journal}}
: Citar diario requiere |journal=
( ayuda )