Hispanopedia Wiki
Articulo de referencia

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 . [1...

Hispanopedia WikiContenido en espanolLectura gratuita

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]

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 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]

Síntesis

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]

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 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.

Verificación de cierre de sesión

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 ]

Prueba dirigida por humanos

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 pasan desapercibidos 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.

Prueba automatizada

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:

  • 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 .
  • Comprobación de modelos , en la que un sistema verifica ciertas propiedades mediante una búsqueda exhaustiva de todos los estados posibles en los 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 de comportamiento del programa, utilizando un cálculo de punto fijo sobre una red (posiblemente completa) que la representa.

Algunos probadores automáticos de teoremas 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.

Técnicas

Los métodos formales incluyen una serie de técnicas diferentes.

Idiomas de especificación

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]

Diagramas de decisión binaria

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] PAG {\displaystyle {\mathcal {P}}} PAG {\displaystyle {\mathcal {P}}}

Solucionadores de SAT

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] PAG {\displaystyle {\mathcal {P}}} ¬ PAG {\displaystyle \neg {\mathcal {P}}}

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 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

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 ]

Métodos semiformales

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]

Métodos formales y notaciones

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

Idiomas de especificación

Comprobadores de modelos

Solucionadores y competiciones

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]

Organizaciones

Véase tambié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. "Why Engineers Should Consider Formal Methods" (PDF) . 16th Digital Avionics Systems Conference (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 citar revista |journal=( ayuda )
  3. ^ Monin, págs. 3-4
  4. ^ Utting, Mark; Reeves, Steve (31 de agosto de 2001). "Enseñanza de métodos formales ligeros mediante pruebas". Pruebas de software, verificación y confiabilidad . 11 (3): 181–195. doi :10.1002/stvr.223.
  5. ^ Backus, JW (1959). "La sintaxis y la semántica del lenguaje algebraico internacional propuesto en la Conferencia ACM-GAMM de Zúrich". Actas de la Conferencia Internacional sobre Procesamiento de la Información . UNESCO.
  6. ^ Knuth, Donald E. (1964), Forma normal de Backus frente a forma de Backus Naur. Comunicaciones de la ACM , 7(12):735–736.
  7. ^ O'Hearn, Peter W.; Tennent, Robert D. (1997). Lenguajes similares a Algol .
  8. ^ Gulwani, Sumit; Polozov, Oleksandr; Singh, Rishabh (2017). "Síntesis de programas". Fundamentos y tendencias en lenguajes de programación . 4 (1–2): 1–119. doi :10.1561/2500000010.
  9. ^ A. Cortesi y M. Zanioli, Operadores de ensanchamiento y estrechamiento para interpretación abstracta. Lenguajes informáticos, sistemas y estructuras. Volumen 37(1), págs. 24–42, Elsevier, ISSN  1477-8424 (2011).
  10. ^ Bjørner, Dines; Henson, Martin C. (2008). Lógica de lenguajes de especificación . págs. VII–XI.
  11. ^ Bryant, Randal E. (2018). "Diagramas de decisión binaria". En Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.). Manual de verificación de modelos . pág. 191.
  12. ^ Chaki, Sagar; Gurfinkel, Arie (2018). "Verificación de modelos simbólicos basada en BDD". En Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.). Manual de verificación de modelos . pág. 191.
  13. ^ Prasad, Mukul R; Biere, Armin; Gupta, Aarti (25 de enero de 2005). "Un estudio de los avances recientes en la verificación formal basada en SAT". Revista internacional sobre herramientas de software para la transferencia de tecnología . 7 (2): 156–173. doi :10.1007/s10009-004-0183-4.
  14. ^ Bjørner, cena; Abuela, cristiana; Oest, Ole N.; Rystrom, Leif (2011). "Centro Dansk Datamatik". En Impagliazzo, Juan; Lundin, Per; Wangler, Benkt (eds.). Historia de la informática nórdica 3: avances del IFIP en tecnologías de la información y las comunicaciones . Saltador. págs. 350–359.
  15. ^ Bjørner, Dines; Havelund, Klaus. "40 años de métodos formales: ¿algunos obstáculos y algunas posibilidades?". FM 2014: Métodos formales: 19.° simposio internacional, Singapur, 12-16 de mayo de 2014. Actas (PDF) . Springer. págs. 42-61.
  16. ^ Gheorghe, AV y Ancel, E. (noviembre de 2008). Integración de sistemas aéreos no tripulados en el sistema de espacio aéreo nacional. En Sistemas y servicios de infraestructura: creación de redes para un futuro más brillante (INFRA), Primera conferencia internacional de 2008 sobre (pp. 1-5). IEEE.
  17. ^ Resolución y detección de conflictos coordinada en el aire, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/ Archivado el 5 de marzo de 2016 en Wayback Machine.
  18. ^ "Taller B". www.atelierb.eu .
  19. ^ 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.
  20. ^ Verificación formal en la validación del motor de ejecución del procesador Intel Core i7, http://cps-vo.org/node/1371 Archivado el 3 de mayo de 2015 en Wayback Machine , consultado el 13 de septiembre de 2013.
  21. ^ J. Grundy, "Optimizaciones verificadas para la arquitectura Intel IA-64", en Demostración de teoremas en lógicas de orden superior, Springer Berlin Heidelberg, 2004, págs. 215-232.
  22. ^ E. Seligman, I. Yarom, "Los métodos más conocidos para utilizar Cadence Conformal LEC", en Intel.
  23. ^ C. Eisner, A. Nahir, K. Yorav, "Verificación funcional de diseños con compuertas de potencia mediante razonamiento compositivo [ enlace muerto permanente ] ", Computer Aided Verification, Springer Berlin Heidelberg, págs. 433–445.
  24. ^ PC Attie, H. Chockler, "Verificación automática de emulaciones de registros tolerantes a fallos", Electronic Notes in Theoretical Computer Science, vol. 149, núm. 1, págs. 49–60.
  25. ^ KD Schubert, W. Roesner, JM Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, "Verificación funcional de los sistemas de microprocesador y multiprocesador POWER7 de IBM", IBM Journal of Research and Development, vol. 55, no 3.
  26. ^ X2R-2, entregable D5.1 .
  27. ^ Daniel Jackson y Jeannette Wing , "Métodos formales ligeros", IEEE Computer , abril de 1996
  28. ^ Vinu George y Rayford Vaughn, "Aplicación de métodos formales ligeros en ingeniería de requisitos" Archivado el 1 de marzo de 2006 en Wayback Machine , Crosstalk: The Journal of Defense Software Engineering , enero de 2003
  29. ^ Daniel Jackson, "Alloy: una notación ligera para modelado de objetos", ACM Transactions on Software Engineering and Methodology (TOSEM) , volumen 11, número 2 (abril de 2002), págs. 256-290
  30. ^ Richard Denney, Cómo tener éxito con los casos de uso: trabajar de forma inteligente para ofrecer calidad , Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6 . 
  31. ^ Sten Agerholm y Peter G. Larsen, "Un enfoque ligero para los métodos formales", archivado el 9 de marzo de 2006 en Wayback Machine , en Actas del Taller internacional sobre tendencias actuales en métodos formales aplicados , Boppard, Alemania, Springer-Verlag, octubre de 1998
  32. ^ "ESBMC". esbmc.org .
  33. ^ Bartocci, Ezio; Beyer, Dirk; Black, Paul E.; Fedyukovich, Grigory; Garavel, Hubert; Hartmanns, Arnd; Huisman, Marieke; Kordon, Fabrice; Nagele, Julian; Sighireanu, Mihaela; Steffen, Bernhard; Suda, Martin; Sutcliffe, Geoff; Weber, Tjark; Yamada, Akihisa (2019). "TOOLympics 2019: una descripción general de las competencias en métodos formales". En Beyer, Dirk; Huisman, Marieke; Kordon, Fabrice; Steffen, Bernhard (eds.). Herramientas y algoritmos para la construcción y análisis de sistemas . Apuntes de clase en informática. Cham: Springer International Publishing. págs. 3–24. doi : 10.1007/978-3-030-17502-3_1 . ISBN 978-3-030-17502-3.
  34. ^ Froleyks, Nils; Heule, Marijn; Iser, Markus; Järvisalo, Matti; Suda, Martín (1 de diciembre de 2021). "Concurso SAT 2020". Inteligencia artificial . 301 : 103572. doi : 10.1016/j.artint.2021.103572 . ISSN  0004-3702.
  35. ^ Cornejo, César (27 de enero de 2021). "Soporte aritmético basado en SAT para aleaciones". Actas de la 35.ª Conferencia Internacional IEEE/ACM sobre Ingeniería de Software Automatizada . ASE '20. Nueva York, NY, EE. UU.: Association for Computing Machinery. págs. 1161–1163. doi :10.1145/3324884.3415285. ISBN 978-1-4503-6768-4.
  36. ^ Barrett, Clark; Deters, Morgan; de Moura, Leonardo; Oliveras, Albert; Stump, Aaron (1 de marzo de 2013). "6 años de SMT-COMP". Revista de razonamiento automatizado . 50 (3): 243–277. doi :10.1007/s10817-012-9246-5. ISSN  1573-0670.
  37. ^ Fedyukovich, Grigory; Rümmer, Philipp (13 de septiembre de 2021). "Informe de competencia: CHC-COMP-21". Actas electrónicas en informática teórica . 344 : 91–108. arXiv : 2008.02939 . doi : 10.4204/EPTCS.344.7 . ISSN  2075-2180.
  38. ^ Shukla, Ankit; Biere, Armin; Pulina, Luca; Seidl, Martina (noviembre de 2019). "Una encuesta sobre aplicaciones de fórmulas booleanas cuantificadas". 2019 IEEE 31st International Conference on Tools with Artificial Intelligence (ICTAI) . IEEE. págs. 78–84. doi :10.1109/ICTAI.2019.00020. ISBN 978-1-7281-3798-8.
  39. ^ Pulina, Luca; Seidl, Martina (1 de septiembre de 2019). "Evaluaciones de los solucionadores QBF de 2016 y 2017 (QBFEVAL'16 y QBFEVAL'17)". Inteligencia artificial . 274 : 224–248. doi : 10.1016/j.artint.2019.04.002 . ISSN  0004-3702.
  40. ^ Beyer, Dirk (2022). "Progreso en la verificación de software: SV-COMP 2022". En Fisman, Dana; Rosu, Grigore (eds.). Herramientas y algoritmos para la construcción y análisis de sistemas . Apuntes de clase en informática. Vol. 13244. Cham: Springer International Publishing. págs. 375–402. doi : 10.1007/978-3-030-99527-0_20 . ISBN . 978-3-030-99527-0.
  41. ^ Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (28 de noviembre de 2017). "SyGuS-Comp 2017: resultados y análisis". Actas electrónicas en informática teórica . 260 : 97–115. arXiv : 1611.07627 . doi : 10.4204/EPTCS.260.9 . ISSN  2075-2180.

Lectura adicional

  • Jonathan P. Bowen y Michael G. Hinchey, Formal Methods . En Allen B. Tucker, Jr. (ed.), Computer Science Handbook , 2.ª edición, Sección XI, Ingeniería de software , Capítulo 106, páginas 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 [ enlace muerto permanente ] . 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: 25.ª conferencia internacional, FMICS 2020 (PDF) . Apuntes de clase en informática (LNCS). Vol. 12327. Springer . págs. 3–69. doi :10.1007/978-3-030-58298-2_1. ISBN 978-3-030-58297-5. Número de identificación del sujeto  221381022.* Michael G. Hinchey, Jonathan P. Bowen y Emil Vassev, Métodos formales . En Philip A. Laplante (ed.), Enciclopedia de ingeniería de software , 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 ingeniería de sistemas confiables: una encuesta a profesionales de Europa y América del Norte". Ingeniería de software empírica . 25 (6). Springer Nature : 4473–4546. arXiv : 1812.08815 . 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 . 
  • Métodos Formales Europa (FME)
  • Wiki de métodos formales
  • Métodos formales de Foldoc
Material de archivo
Obtenido de "https://es.wikipedia.org/w/index.php?title=Métodos_formales&oldid=1241059659"
Lecturas relacionadas
6 articulos
Ciencias de la ComputaciónCiencias de la ComputaciónÁreas fundamentales de la informática La informática es el estudio de la computación , la información y la automatización . [1] [2] [3] La informát...MatemáticasMatemáticasLas matemáticas son un campo de estudio que descubre y organiza métodos, teorías y teoremas que se desarrollan y prueban para las necesidades de la...Especificación formalEn informática , las especificaciones formales son técnicas basadas en matemáticas cuyo propósito es ayudar con la implementación de sistemas y sof...Análisis del programaAnálisis del programaEn informática , el análisis de programas [1] es el proceso de analizar automáticamente el comportamiento de los programas informáticos en relación...Verificación formalEn el contexto de los sistemas de hardware y software , la verificación formal es el acto de probar o refutar la corrección de un sistema con respe...SoftwareSoftwareEl software consiste en programas informáticos que dan instrucciones sobre la ejecución de una computadora . [1] El software puede definirse de man...