Métodos formales

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. 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 la ingeniería, realizar un análisis matemático adecuado puede contribuir a la confiabilidad y solidez de un diseño.

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.

Antecedentes

Los métodos semiformales son formalismos y lenguajes que no se consideran totalmente "formales". Aplaza la tarea de completar la semántica a 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.

Taxonomía

Los métodos formales se pueden utilizar en varios niveles:

• Nivel 0: La especificación formal se puede llevar a cabo y luego un programa desarrollado de esta manera informal. Esto ha sido apuñalado formal methods lite. Esta puede ser la opción más rentable en muchos casos.
• Nivel 1: El desarrollo formal y la verificación formal pueden utilizarse para producir un programa de manera más formal. Por ejemplo, se pueden realizar pruebas de propiedades o refinamiento de la especificación a un programa. Esto puede ser más apropiado en sistemas de alta integridad que implican seguridad o seguridad.
• Nivel 2: Los proversores de teorema pueden utilizarse para llevar a cabo pruebas totalmente formales de verificación automática. A pesar de mejorar las herramientas y reducir los costos, esto puede ser muy caro y sólo vale prácticamente la pena si el costo de los errores es muy alto (por ejemplo, en partes críticas del sistema operativo o el diseño del microprocesador).

Más información sobre esto se amplía a continuación.

Al igual que con la semántica del lenguaje de programación, los estilos de los métodos formales pueden clasificarse aproximadamente de la siguiente manera:

• Semántica denotacional, en la que el significado de un sistema se expresa en la teoría matemática de los dominios. Los partidarios de tales métodos dependen de la naturaleza bien comprendida de los dominios para dar sentido al sistema; los críticos señalan que no todo sistema puede ser visto intuitiva o naturalmente como una función.
• Semántica operacional, en la que el significado de un sistema se expresa como una secuencia de acciones de un modelo computacional (presumiblemente) más simple. Los partidarios de tales métodos apuntan a la sencillez de sus modelos como un medio para la claridad expresiva; los críticos contradicen que el problema de la semántica se ha retrasado (¿quién define la semántica del modelo más simple?).
• Semántica axiomática, en la que se expresa el significado del sistema en términos de condiciones previas y condiciones posteriores que son verdaderas antes y después de que el sistema realice una tarea, respectivamente. Los partidarios señalan la conexión con la lógica clásica; los críticos señalan que tal semántica nunca describe realmente lo que un sistema ¿Sí? (meremente lo que es cierto antes y después).

Métodos formales ligeros

Algunos profesionales creen que la comunidad de métodos formales ha enfatizado demasiado la formalización completa de una especificación o diseño. 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. Los ejemplos de este enfoque ligero de los métodos formales incluyen la notación de modelado de objetos de aleación, la síntesis de Denney de algunos aspectos de la notación Z con desarrollo basado en casos de uso y las herramientas CSK VDM.

Usos

Los métodos formales se pueden aplicar en varios puntos del proceso de desarrollo.

Especificación

Se pueden utilizar métodos formales para dar una descripción del sistema a desarrollar, en cualquier nivel de detalle que se desee. Esta descripción formal se puede utilizar para orientar las actividades de desarrollo posteriores (consulte las siguientes secciones); además, se puede utilizar para verificar que los requisitos del sistema que se está desarrollando se han especificado de forma completa y precisa, o formalizar los requisitos del sistema expresándolos en un lenguaje formal con una sintaxis y una semántica precisas y sin ambigüedades definidas.

Durante años se ha observado la necesidad de sistemas de especificación formales. En el informe ALGOL 58, 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). 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. "Por lo tanto, el tratamiento formal de la semántica de los programas legales se incluirá en un artículo posterior." Nunca apareció.

Desarrollo

El desarrollo formal es el uso de métodos formales como una parte integrada de un proceso de desarrollo de sistemas respaldado por herramientas.

Una vez que se ha producido una especificación formal, la especificación se puede utilizar como guía mientras se desarrolla el sistema concreto durante el proceso de diseño (es decir, realizado típicamente en software, pero también potencialmente en hardware). Por ejemplo:

• Si la especificación formal está en la semántica operacional, el comportamiento observado del sistema concreto puede compararse con el comportamiento de la especificación (que en sí debe ser ejecutable o simulable). Además, los comandos operativos de la especificación pueden ser amenibles para la traducción directa al código ejecutable.
• Si la especificación formal está en la semántica axiomática, las condiciones previas y posteriores de la especificación pueden convertirse en afirmaciones en el código ejecutable.

Verificación

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 implementación de un sistema satisface su especificación.

Una vez que se ha desarrollado una especificación formal, la especificación se puede utilizar como base para probar las propiedades de la especificación y, por inferencia, las propiedades de la implementación del sistema.

Verificación de cierre

La verificación de aprobación es el uso de una herramienta de verificación formal que es altamente confiable. Tal herramienta puede reemplazar los métodos de verificación tradicionales (la herramienta puede incluso estar certificada).

Prueba dirigida por humanos

A veces, la motivación para probar 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 compuestas) usando lenguaje natural, usando un nivel de informalidad común a tales pruebas. Un "bueno" 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, los errores sutiles pueden estar presentes en los detalles de bajo nivel que normalmente se pasan por alto en tales pruebas. Además, el trabajo involucrado en la producción de una prueba tan buena requiere un alto nivel de sofisticación y experiencia matemática.

Prueba automatizada

Por el contrario, hay un interés creciente en la producción de pruebas de corrección de tales sistemas por medios automatizados. Las técnicas automatizadas se dividen en tres categorías generales:

• Teorema automatizado, en el que un sistema intenta producir una prueba formal desde cero, dada una descripción del sistema, un conjunto de axiomas lógicos, y un conjunto de reglas de inferencia.
• Verificación de modelos, en la que un sistema verifica ciertas propiedades mediante una búsqueda exhaustiva de todos los estados posibles que un sistema podría entrar durante su ejecución.
• Interpretación abstracta, en la que un sistema verifica una sobreaproximación de una propiedad conductual del programa, utilizando una computación de punto fijo sobre una celosía (posiblemente completa).

Algunos probadores de teoremas automatizados requieren orientación sobre qué propiedades son "interesantes" suficiente para perseguir, mientras que otros trabajan 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 lo suficientemente abstracto.

Los defensores de tales sistemas argumentan que los resultados tienen una mayor certeza matemática que las demostraciones producidas por humanos, ya que todos los tediosos detalles han sido verificados algorítmicamente. El entrenamiento requerido para usar tales sistemas también es menor que el requerido para producir buenas demostraciones matemáticas a mano, haciendo 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 una 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 producidos. Algunas herramientas modernas de verificación de modelos producen un "registro de prueba" detallando cada paso en su prueba, haciendo posible 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, no se devuelven falsos negativos. Además, es eficientemente escalable, ajustando el dominio abstracto que representa la propiedad a analizar y aplicando operadores de ampliación para obtener una convergencia rápida.

Aplicaciones

Los métodos formales se aplican en diferentes áreas de hardware y software, incluidos enrutadores, conmutadores Ethernet, protocolos de enrutamiento, aplicaciones de seguridad y micronúcleos de sistemas operativos como seL4. Hay varios ejemplos en los que se han utilizado para verificar la funcionalidad del hardware y el software utilizados en los DC. IBM utilizó ACL2, un probador de teoremas, en el proceso de desarrollo del procesador AMD x86. Intel utiliza dichos métodos para verificar su hardware y firmware (software permanente programado en una memoria de solo lectura). 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.

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, la integración del Sistema de Aeronaves No Tripuladas en el Sistema Nacional del Espacio Aéreo y la Resolución y Detección Coordinada de Conflictos Aerotransportados (ACCoRD). B-Method con Atelier B, 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, utilizan con frecuencia la verificación formal en el hardware. Hay muchas áreas de hardware en las que Intel ha utilizado FM para verificar el funcionamiento de los productos, como la verificación parametrizada del protocolo coherente con la memoria caché, la validación del motor de ejecución del procesador Intel Core i7 (mediante la prueba de teoremas, BDD y evaluación simbólica), la optimización para la arquitectura Intel IA-64 mediante el comprobador de teoremas ligeros HOL y la verificación del controlador Gigabit Ethernet de dos puertos de alto rendimiento compatible con el protocolo PCI Express y la tecnología de gestión avanzada de Intel mediante Cadence. De manera similar, IBM ha utilizado métodos formales en la verificación de puertas de energía, registros y verificación funcional del microprocesador IBM Power7.

En desarrollo de software

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 o 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 a través de la 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 la programación funcional, las pruebas basadas en propiedades han permitido la especificación matemática y las pruebas (si no pruebas exhaustivas) del comportamiento esperado de las funciones individuales.

El lenguaje de restricción de objetos (y especializaciones como el lenguaje de modelado de Java) ha permitido que los sistemas orientados a objetos se especifiquen formalmente, aunque no necesariamente se verifiquen formalmente.

Para software y sistemas simultáneos, 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 controlada por eventos) permiten la especificación de software ejecutable y se pueden usar 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 algún tipo de lógica, generalmente una variación de la lógica de primer orden (FOL), y luego ejecutar directamente la lógica como si fuera un programa. El lenguaje OWL, basado en la Lógica de Descripción (DL), es un ejemplo. También se trabaja en el mapeo automático de alguna versión del inglés (u otro idioma natural) hacia y desde la lógica, así como la ejecución de la lógica directamente. Ejemplos son Attempto Controlled English e Internet Business Logic, que no buscan controlar el vocabulario o la sintaxis. Una característica de los sistemas que admiten el mapeo lógico bidireccional en inglés y la ejecución directa de la lógica es que se pueden hacer para explicar sus resultados, en inglés, a nivel comercial o científico.

Métodos formales y notaciones

Hay una variedad de métodos formales y notaciones disponibles.

Idiomas de especificación

• Abstract State Machines (ASMs)
• Lógica Computacional para Lisp Común Aplicable (ACL2)
• Modelo Actor
• Aleación
• Lenguaje de especificación ANSI/ISO C (ACSL)
• Lenguaje de especificación del sistema autonómico (ASSL)
• B-Method
• CADP
• Lenguaje de especificación algebraica común (CASL)
• Esterel
• Java Modeling Language (JML)
• Auxiliar de Software Basado en Conocimientos (KBSA)
• Lustre
• mCRL2
• Perfect Developer
• Redes Petri
• Programación preventiva
• Calculi de proceso
  • CSP
  • LOTOS
  • π-calculus
• RAISE
• Rebeca Modeling Language
• SPARK Ada
• Especificación y descripción del idioma
• TLA+
• USL
• VDM
  • VDM-SL
  • VDM++
• Z notación

Modelo de damas

• ESBMC
• MALPAS Herramientas de Análisis Estatico de Software – un modelo de fuerza industrial utilizado para la prueba formal de sistemas críticos de seguridad
• PAT – un control de modelos gratuito, simulador y control de refinamiento para sistemas concurrentes y extensiones CSP (por ejemplo, variables compartidas, arrays, equidad)
• SPIN
• UPPAAL

Organizaciones

• BCS-FACS
• Métodos formales Europa
• Z User Group