De Wikipedia, la enciclopedia libre
Ir a navegaciónSaltar a buscar

En ciencias de la computación , específicamente ingeniería de software e ingeniería de hardware , los métodos formales son un tipo particular de técnicas matemáticamente rigurosas para la especificación , desarrollo 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 la 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 se describen mejor como la aplicación de un bastante amplia variedad de la informática teórica fundamentales, en particular la lógica cálculos, los lenguajes formales , la teoría de autómatas , sistema de eventos dinámicos discretos y la semántica del programa , sino también de tipo de sistemas y tipos de datos algebraicos a los problemas en el software y especificación y verificación de hardware. [3]

Antecedentes

Los métodos semiformales son formalismos y lenguajes que no se consideran completamente “ 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. [4]

Taxonomía

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

Nivel 0: Se puede realizar una especificación formal y luego se puede desarrollar un programa a partir de esto de manera informal. Esto se ha denominado métodos formales lite . Esta puede ser la opción más rentable en muchos casos.

Nivel 1: El desarrollo formal y la verificación formal se pueden utilizar para producir un programa de una 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 involucran seguridad o protección .

Nivel 2: Los probadores de teoremas pueden usarse para realizar pruebas completamente formales verificadas por máquina. A pesar de mejorar las herramientas y reducir los costos, esto puede ser muy costoso y solo vale la pena en la práctica 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 métodos formales se pueden clasificar de la siguiente manera:

  • Semántica denotacional , en la que el significado de un sistema se expresa en la teoría matemática de dominios . Los defensores de tales métodos se basan en la naturaleza bien entendida de los dominios para dar significado al sistema; los críticos señalan que no todos los sistemas pueden verse 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 defensores de tales métodos señalan la simplicidad de sus modelos como un medio de claridad expresiva; los críticos responden que el problema de la semántica acaba de retrasarse (¿quién define la semántica del modelo más simple?).
  • Semántica axiomática , en la que el significado del sistema se expresa en términos de precondiciones y poscondiciones que son verdaderas antes y después de que el sistema realice una tarea, respectivamente. Los defensores notan la conexión con la lógica clásica ; los críticos señalan que este tipo de semántica en realidad nunca lo describen un sistema que hace (meramente lo que es cierto, antes y después).

Métodos formales ligeros

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. [5] [6] 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 focalizada. Ejemplos de este enfoque ligero para los métodos formales incluyen la notación de modelado de objetos de aleación , [7] la síntesis de Denney de algunos aspectos de la notación Z con desarrollo basado en casos de uso , [8]y las herramientas CSK VDM . [9]

Usos

Los métodos formales se pueden aplicar en varios puntos durante el 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 deseado. Esta descripción formal se puede utilizar para orientar las actividades de desarrollo posteriores (consulte las secciones siguientes); Además, se puede utilizar para verificar que los requisitos para el sistema que se está desarrollando se hayan especificado de forma completa y precisa, o para formalizar los requisitos del sistema expresándolos en un lenguaje formal con una sintaxis y una semántica precisas e inequívocamente definidas.

Durante años se ha observado la necesidad de sistemas formales de especificación. En el informe ALGOL 58 , [10] John Backus presentó una notación formal para describir la sintaxis del lenguaje de programación, posteriormente denominada forma normal de Backus y luego rebautizada como forma Backus-Naur (BNF). [11] 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 parte integral de un proceso de desarrollo de sistemas apoyado por herramientas.

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

  • Si la especificación formal está en semántica operativa, el comportamiento observado del sistema concreto puede compararse con el comportamiento de la especificación (que en sí misma debería ser ejecutable o simulable). Además, los comandos operativos de la especificación pueden ser susceptibles de traducción directa en código ejecutable.
  • Si la especificación formal está en semántica axiomática, las precondiciones y poscondiciones 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 puede usarse como base para probar las propiedades de la especificación (y, con suerte, por inferencia el sistema desarrollado).

Verificación de aprobación

La verificación de aprobación es el uso de una herramienta de verificación formal que es altamente confiable. Dicha 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 estar seguro de la corrección del sistema, sino el deseo de comprender mejor el sistema. En consecuencia, algunas pruebas de corrección se producen en el estilo de la prueba matemática : escritas a mano (o compuestas) usando lenguaje natural , usando 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 los errores no se detecten en tales demostraciones; A menudo, pueden estar presentes errores sutiles en los detalles de bajo nivel que normalmente se pasan por alto en tales pruebas. Además, el trabajo involucrado en producir una prueba tan buena requiere un alto nivel de sofisticación y experiencia matemática.

Prueba automatizada

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

  • Demostración automatizada de teoremas , en la 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 determinadas propiedades mediante una búsqueda exhaustiva de todos los estados posibles en los que podría entrar un sistema durante su ejecución.
  • Interpretación abstracta , en la que un sistema verifica una sobreaproximación de una propiedad de comportamiento del programa, utilizando un cálculo de punto fijo sobre un enrejado (posiblemente completo) que lo representa.

Algunos probadores automatizados de teoremas requieren orientación sobre qué propiedades son lo suficientemente "interesantes" para seguir, 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 da 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 se han verificado algorítmicamente. La formación necesaria para utilizar estos sistemas también es menor que la necesaria 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 de 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 en sí mismo, puede haber razones para dudar de la solidez de los resultados producidos. Algunas herramientas modernas de verificación de modelos producen un "registro de pruebas" 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, no se devuelven falsos negativos. Además, es escalable de manera eficiente, ajustando el dominio abstracto que representa la propiedad a analizar y aplicando operadores de ampliación [12] 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 microkernels del sistema operativo como seL4 . Hay varios ejemplos en los que se han utilizado para verificar la funcionalidad del hardware y el software utilizados en los países en desarrollo [ aclaración necesaria ] . IBM usó ACL2 , un demostrador de teoremas, en el proceso de desarrollo del procesador AMD x86. [ cita requerida ] Intel utiliza tales métodos para verificar su hardware y firmware (software permanente programado en una memoria de sólo 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. [13] [14]

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 del Espacio Aéreo Nacional [15] y la Resolución y Detección Coordinada de Conflictos Aerotransportados (ACCoRD). [16] B-Method con Atelier B , [17] se utiliza para desarrollar automatismos de seguridad para los distintos subterráneos 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 ySTMicroelectronics .

La verificación formal se ha utilizado con frecuencia en hardware por la mayoría de los proveedores de hardware conocidos, como IBM, Intel y AMD. 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 en caché, [18] validación del motor de ejecución del procesador Intel Core i7 [19] (utilizando pruebas de teoremas, BDD , y evaluación simbólica), optimización para la arquitectura Intel IA-64 usando el comprobador de teoremas de luz HOL, [20] y verificación de un controlador Ethernet gigabit de puerto dual de alto rendimiento con soporte para el protocolo PCI Express y la tecnología de administración avanzada de Intel usando Cadence. [21]De manera similar, IBM ha utilizado métodos formales en la verificación de puertas de energía, [22] registros, [23] y verificación funcional del microprocesador IBM Power7. [24]

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, 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 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 la suplementació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 la B-Método , los lenguajes de especificación utilizados en demostración automática 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 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 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 la máquina virtual de estados finitos o la máquina de estados finitos dirigida por eventos ) permiten la especificación de software ejecutable y se pueden usar 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 (FOL), y luego ejecutar directamente la lógica como si fuera un programa. El lenguaje OWL , basado en Description Logic (DL), es un ejemplo. También se trabaja en mapear alguna versión del inglés (u otro lenguaje natural) automáticamente hacia y desde la lógica, así como ejecutar la lógica directamente. Ejemplos son Intento de inglés controladoe Internet Business Logic, que no buscan controlar el vocabulario ni la sintaxis. Una característica de los sistemas que admiten el mapeo bidireccional de la lógica inglesa y la ejecución directa de la lógica es que se pueden hacer para explicar sus resultados, en inglés, a nivel empresarial o científico. [ cita requerida ]

Métodos y notaciones formales

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

Idiomas de especificación

  • Máquinas de estado abstracto (ASM)
  • Una lógica computacional para Common Lisp aplicativo (ACL2)
  • Modelo de actor
  • Aleación
  • Lenguaje de especificación ANSI / ISO C (ACSL)
  • Lenguaje de especificación del sistema autónomo (ASSL)
  • Método B
  • CADP
  • Lenguaje común de especificación algebraica (CASL)
  • Esterel
  • Lenguaje de modelado Java (JML)
  • Asistente de software basado en conocimientos (KBSA)
  • Lustre
  • mCRL2
  • Desarrollador perfecto
  • Redes de Petri
  • Programación predicativa
  • Cálculos de proceso
    • CSP
    • LOTO
    • π-cálculo
  • AUMENTAR
  • Lenguaje de modelado de Rebeca
  • CHISPA Ada
  • Especificación aguda (Especificación #)
  • Lenguaje de especificación y descripción
  • TLA +
  • USL
  • VDM
    • VDM-SL
    • VDM ++
  • Notación Z

Verificadores de modelos

  • ESBMC [25]
  • Conjunto de herramientas de análisis estático de software MALPAS : un comprobador de modelos de resistencia industrial que se utiliza para pruebas formales de sistemas críticos para la seguridad.
  • PAT : un verificador de modelos, simulador y verificador de refinamiento gratuito para sistemas concurrentes y extensiones CSP (por ejemplo, variables compartidas, matrices, equidad)
  • VUELTA
  • UPPAAL

Organizaciones

  • APCB
  • BCS-FACS
  • Métodos formales Europa
  • Grupo de usuarios Z

Ver también

  • Interpretación abstracta
  • Demostración automatizada de teoremas
  • Diseño por contrato
  • Métodos formales personas
  • Especificación formal
  • Verificación formal
  • Sistema formal
  • Comprobación de modelo
  • Ingeniería de software
  • Lenguaje de especificación

Referencias

  1. ↑ Butler, RW (6 de agosto de 2001). "¿Qué son los métodos formales?" . Consultado el 16 de noviembre de 2006 .
  2. ^ Holloway, C. Michael. "Por qué los ingenieros deberían considerar métodos formales" (PDF) . 16ª Conferencia sobre sistemas de aviónica digital (27-30 de octubre de 1997). Archivado desde el original (PDF) el 16 de noviembre de 2006 . Consultado el 16 de noviembre de 2006 . Cite journal requiere |journal=( ayuda )
  3. ^ Monin, págs. 3-4
  4. ^ X2R-2, entregable D5.1 .
  5. ^ Daniel Jackson y Jeannette Wing , "Métodos formales ligeros" , Computadora IEEE , abril de 1996
  6. ^ Vinu George y Rayford Vaughn, "Aplicación de métodos formales ligeros en ingeniería de requisitos" Archivado el 1 demarzo de 2006en Wayback Machine , Crosstalk: The Journal of Defense Software Engineering , enero de 2003
  7. ^ Daniel Jackson, "Aleación: una notación de modelado de objetos ligeros" , Transacciones de ACM sobre ingeniería de software y metodología (TOSEM) , volumen 11, número 2 (abril de 2002), págs. 256-290
  8. ^ Richard Denney, Tener éxito con los casos de uso: trabajar de manera inteligente para ofrecer calidad , Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6 . 
  9. ^ Sten Agerholm y Peter G. Larsen, "Un enfoque ligero de los métodos formales" Archivado el 9 de marzo de 2006 en la Wayback Machine , en las actas del Taller internacional sobre las tendencias actuales en los métodos formales aplicados , Boppard, Alemania, Springer-Verlag, Octubre de 1998
  10. ^ Backus, JW (1959). "La sintaxis y semántica de la propuesta de lenguaje algebraico internacional de Zürich Conferencia ACM-GAMM". Actas de la Conferencia Internacional sobre Procesamiento de Información . UNESCO.
  11. ^ Knuth, Donald E. (1964), Forma normal de Backus vs Forma de Backus Naur. Comunicaciones del ACM , 7 (12): 735–736.
  12. ^ A. Cortesi y M. Zanioli, Operadores de ensanchamiento y estrechamiento para interpretación abstracta . Lenguajes, sistemas y estructuras informáticas. Volumen 37 (1), págs. 24–42, Elsevier, ISSN 1477-8424 (2011). 
  13. ^ Bjørner, Dines; Gram, Christian; Oest, Ole N .; Rystrøm, Leif (2011). "Centro Dansk Datamatik". En Impagliazzo, John; Lundin, Per; Wangler, Benkt (eds.). Historia de la Computación Nórdica 3: Avances de IFIP en tecnología de la información y la comunicación . Saltador. págs. 350–359.
  14. ^ Bjørner, Dines; Havelund, Klaus. "40 años de métodos formales: ¿algunos obstáculos y algunas posibilidades?". FM 2014: Métodos formales: XIX Simposio internacional, Singapur, 12 al 16 de mayo de 2014. Actas (PDF) . Saltador. págs. 42–61.
  15. ^ Gheorghe, AV y Ancel, E. (2008, noviembre). Integración de sistemas aéreos no tripulados al Sistema Nacional del Espacio Aéreo. En Sistemas y servicios de infraestructura: Construyendo redes para un futuro más brillante (INFRA), Primera Conferencia Internacional de 2008 sobre (págs. 1-5). IEEE.
  16. ^ Detección y resolución coordinada de conflictos en el aire, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/
  17. ^ "Atelier B" . www.atelierb.eu .
  18. ^ CT Chou, PK Mannava, S. Park, " Un método simple para la verificación parametrizada de protocolos de coherencia de caché ", Métodos formales en diseño asistido por computadora, págs. 382–398, 2004.
  19. ^ Verificación formal en la validación del motor de ejecución del procesador Intel® Core ™ i7, http://cps-vo.org/node/1371 , consultado el 13 de septiembre de 2013.
  20. ^ J. Grundy, "Optimizaciones verificadas para la arquitectura Intel IA-64", en prueba de teoremas en lógicas de orden superior, Springer Berlín Heidelberg, 2004, págs. 215-232.
  21. ^ E. Seligman, I. Yarom, " Los métodos más conocidos para usar LEC conforme a la cadencia ", en Intel.
  22. ^ C. Eisner, A. Nahir, K. Yorav, " Verificación funcional de diseños con compuerta de energía mediante razonamiento compositivo ", Verificación asistida por computadora, Springer Berlin Heidelberg, págs. 433–445.
  23. ^ PC Attie, H. Chockler, " Verificación automática de emulaciones de registro tolerantes a fallas ", Notas electrónicas en informática teórica, vol. 149, no. 1, págs. 49–60.
  24. ^ KD Schubert, W. Roesner, JM Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, " Verificación funcional del microprocesador IBM POWER7 y sistemas multiprocesador POWER7 ", IBM Journal of Research and Development, vol. 55, no 3.
  25. ^ "ESBMC" . esbmc.org .
  • Este artículo se basa en material extraído del Diccionario gratuito de informática en línea antes del 1 de noviembre de 2008 e incorporado bajo los términos de "renovación de licencias" de la GFDL , versión 1.3 o posterior.

Lectura adicional

  • Jonathan P. Bowen y Michael G. Hinchey, Métodos formales . En Allen B. Tucker, Jr. (ed.), Computer Science Handbook , 2nd edition, Section XI, Software Engineering , Chapter 106, pages 106-1 - 106-25, Chapman & Hall / CRC Press , Association for Computing Machinery , 2004.
  • Hubert Garavel (editor) y Susanne Graf. Métodos formales para sistemas informáticos seguros y protegidos . Bundesamt für Sicherheit in der Informationstechnik , estudio BSI 875, Bonn, Alemania, diciembre de 2013.
  • Garavel, Hubert; ter Beek, Maurice H .; van de Pol, Jaco (29 de agosto de 2020). "Encuesta de expertos de 2020 sobre métodos formales". Métodos formales para sistemas críticos industriales (PDF) . Lecture Notes in Computer Science (LNCS). 12327 . Springer . págs. 3-69. doi : 10.1007 / 978-3-030-58298-2_1 . ISBN 978-3-030-58297-5. Parámetro desconocido |book-title=ignorado ( ayuda ) * Michael G. Hinchey, Jonathan P. Bowen y Emil Vassev, Métodos formales . En Philip A. Laplante (ed.), Encyclopedia of Software Engineering , Taylor & Francis , 2010, páginas 308–320.
  • Marieke Huisman , Dilian Gurov y Alexander Malkis, Métodos formales: de la academia a la práctica industrial - Una guía de viaje , arXiv: 2002.07279, 2020.
  • Gleirscher, Mario; Marmsoler, Diego (9 de septiembre de 2020). "Métodos formales en la ingeniería de sistemas confiables: una encuesta de profesionales de Europa y América del Norte" . Ingeniería de software empírica . Springer Nature . 25 (6): 4473–4546. doi : 10.1007 / s10664-020-09836-5 .
  • Jean François Monin y Michael G. Hinchey , Comprensión de los métodos formales , Springer , 2003, ISBN 1-85233-247-6 . 

Enlaces externos

  • Métodos formales Europa (FME)
  • Wiki de métodos formales
  • Métodos formales de Foldoc
Material de archivo
  • Palabra clave de método formal en Microsoft Academic Search a través de Archive.org
  • Evidencia sobre los usos y el impacto de los métodos formales en la industria respaldada por el proyecto DEPLOY (EU FP7) en Archive.org