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 , el desarrollo, el análisis y la verificación de sistemas de software y hard...

Hispanopedia WikiContenido en espanolLectura gratuita

En informática , los métodos formales son técnicas matemáticamente rigurosas para la especificación , el desarrollo, el análisis y la verificación de sistemas de software y hardware . [ 1 ] El uso de métodos formales para el diseño de software y hardware se basa en la expectativa de que, al igual que en otras disciplinas de ingeniería, realizar un análisis matemático apropiado puede contribuir a la fiabilidad y robustez de un diseño. [ 2 ]

Los métodos formales emplean una variedad de fundamentos teóricos de la informática , incluyendo 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 pueden aplicarse en varios puntos del proceso de desarrollo .

Especificación

Se pueden utilizar métodos formales para describir formalmente el sistema que se va a desarrollar, con el nivel de detalle deseado. Otros métodos formales pueden basarse en esta especificación para sintetizar un programa o verificar la corrección del sistema.

Alternativamente, la especificación puede ser la única etapa en la que se utilizan métodos formales. Al redactar 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 ]

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

Síntesis

La síntesis de programas es el proceso de crear automáticamente un programa que cumpla con 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 programas posibles para encontrar un programa que sea 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 ]

Verificación

La verificación formal consiste en el uso de herramientas de software para probar las propiedades de una especificación formal, o para demostrar que un modelo formal de la implementación de un sistema satisface su especificación.

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

Verificación de firma

La verificación de aprobación consiste en el uso de una herramienta de verificación formal de alta confianza. Dicha herramienta puede reemplazar los métodos de verificación tradicionales (incluso puede estar certificada). [ 9 ]

Prueba dirigida por humanos

En ocasiones, la motivación para demostrar la corrección de un sistema no reside en la necesidad obvia de confirmar dicha corrección, sino en el deseo de comprenderlo mejor. Por consiguiente, algunas pruebas de corrección se elaboran al estilo de las pruebas matemáticas : manuscritas (o impresas) en lenguaje natural , con un nivel de informalidad propio de este tipo de pruebas. Una buena prueba es aquella que resulta 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 los errores pasen desapercibidos en dichas demostraciones; a menudo, pueden existir errores sutiles en detalles de bajo nivel que suelen pasarse por alto en este tipo de 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

Por el contrario, existe un interés creciente en producir pruebas de 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 demostración formal desde cero, a partir de una descripción del sistema, un conjunto de axiomas lógicos y un conjunto de reglas de inferencia .
  • La verificación de modelos consiste en que un sistema comprueba ciertas propiedades mediante una búsqueda exhaustiva de todos los estados posibles en los que 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 retícula (posiblemente completa) que la representa.

Algunos demostradores automáticos de teoremas requieren orientación sobre 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 al comprobar millones de estados poco interesantes si no se les proporciona un modelo suficientemente abstracto.

Quienes defienden estos sistemas argumentan que los resultados tienen mayor certeza matemática que las demostraciones manuales, ya que todos los detalles minuciosos se han verificado algorítmicamente. Además, la formación necesaria para utilizarlos es menor que la requerida para realizar buenas demostraciones matemáticas a mano, lo que hace que estas técnicas sean accesibles a un mayor número de profesionales.

Los críticos señalan que algunos de estos sistemas son como oráculos : proclaman una verdad, pero no la explican. También existe 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 fiabilidad de los resultados obtenidos. Algunas herramientas modernas de verificación de modelos generan un "registro de prueba" que detalla cada paso de la misma, lo que permite realizar una verificación independiente con las herramientas adecuadas.

La principal característica del enfoque de interpretación abstracta es que proporciona un análisis sólido, es decir, no genera falsos negativos. Además, es eficientemente escalable, ya que permite ajustar el dominio abstracto que representa la propiedad a analizar y aplicar operadores de ampliación [ 10 ] para lograr una convergencia rápida.

Técnicas

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

Lenguajes de especificación

El diseño de un sistema informático puede expresarse mediante un lenguaje de especificación, que es un lenguaje formal que incluye un sistema de prueba. Mediante este sistema de prueba, las herramientas de verificación formal pueden razonar sobre la especificación y establecer que un sistema se ajusta a ella. [ 11 ]

Diagramas de decisión binaria

Un diagrama de decisión binaria es una estructura de datos que representa una función booleana . [ 12 ] Si una fórmula booleanaPAG{\displaystyle {\mathcal {P}}}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 siPAG{\displaystyle {\mathcal {P}}}es una tautología; es decir, siempre se evalúa como VERDADERO. Si este es el caso, entonces el programa siempre cumple con la especificación. [ 13 ]

solucionadores SAT

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 booleanaPAG{\displaystyle {\mathcal {P}}}expresa que una ejecución específica de un programa se ajusta a la especificación, luego determina que¬PAG{\displaystyle \neg {\mathcal {P}}}La condición de insatisfacibilidad equivale 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 acotada, pero también pueden utilizarse en la verificación de modelos no acotada. [ 14 ]

Aplicaciones

Los métodos formales se aplican en diferentes áreas de hardware y software, incluyendo 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 empleados en centros de datos . IBM utilizó ACL2 , un demostrador de teoremas, en el proceso de desarrollo del procesador AMD x86. Intel utiliza estos 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 posteriormente se convirtió en un producto comercial de larga duración. [ 15 ] [ 16 ]

Hay 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, [ 17 ] y la Resolución y Detección Coordinada de Conflictos Aerotransportados (ACCoRD). [ 18 ] El método B con Atelier B , [ 19 ] se utiliza para desarrollar automatismos de seguridad para los diversos metros instalados en todo el mundo por Alstom y Siemens , y también para la certificación de Criterios Comunes 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 más conocidos, como IBM, Intel y AMD. Existen 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 de coherencia de caché, [ 20 ] la validación del motor de ejecución del procesador Intel Core i7 [ 21 ] (utilizando demostración de teoremas, BDD y evaluación simbólica), la optimización para la arquitectura Intel IA-64 utilizando el demostrador de teoremas HOL light, [ 22 ] 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 utilizando Cadence. [ 23 ] De manera similar, IBM ha utilizado métodos formales en la verificación de puertas de potencia, [ 24 ] registros, [ 25 ] y verificación funcional del microprocesador IBM Power7. [ 26 ]

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 las fases 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 . Las normas de garantía de seguridad del software, como la DO-178C, permiten el uso de métodos formales mediante su complementación, y los Criterios Comunes exigen métodos formales en los niveles más altos de categorización.

En el caso del software secuencial, algunos 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 la programación funcional , las pruebas basadas en propiedades han permitido la especificación matemática y la comprobación (si no la comprobación exhaustiva) del comportamiento esperado de las funciones individuales.

El lenguaje de restricciones de objetos (y especializaciones como el lenguaje de modelado de Java ) ha permitido especificar formalmente los sistemas orientados a objetos, aunque no necesariamente verificarlos 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 ; véase 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 pueden utilizarse para construir y validar el comportamiento de la aplicación.

Otro enfoque para 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— y luego ejecutar directamente la lógica como si fuera un programa. El lenguaje OWL , basado en la lógica descriptiva , es un ejemplo. También se está trabajando en el mapeo automático de alguna versión del inglés (u otro lenguaje natural) a la lógica y viceversa, así como en la ejecución directa de la lógica. 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ógica y la ejecución directa de la lógica es que pueden explicar sus resultados, en inglés, a nivel empresarial o científico.

Métodos semiformales

Los métodos semiformales son formalismos y lenguajes que no se consideran completamente "formales". Posponen la tarea de completar la semántica a una etapa posterior, que se realiza mediante interpretación humana o mediante interpretación a través de software como generadores de código o casos de prueba . [ 27 ]

Algunos profesionales creen que la comunidad de métodos formales ha dado demasiada importancia a la formalización completa de una especificación o diseño. [ 28 ] [ 29 ] 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 de los métodos formales incluyen la notación de modelado de objetos Alloy , [ 30 ] la síntesis de Denney de algunos aspectos de la notación Z con desarrollo dirigido por casos de uso , [ 31 ] y las herramientas CSK VDM . [ 32 ]

Métodos y notaciones formales

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

Lenguajes de especificación

Verificadores de modelos

  • ESBMC [ 33 ]
  • FizzBee [ 34 ]
  • MALPAS Software Static Analysis Toolset : un verificador de modelos de nivel industrial utilizado para la prueba formal 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).
  • GIRAR
  • UPPAAL

Solucionadores y competiciones

Muchos problemas en métodos formales son NP-difíciles , pero pueden resolverse en casos que surgen en la práctica. Por ejemplo, el problema de satisfacibilidad booleana es NP-completo según el teorema de Cook-Levin , pero los solucionadores SAT pueden resolver una variedad de instancias grandes. Existen "solucionadores" para diversos problemas que surgen en métodos formales, y se realizan muchas competiciones periódicas para evaluar el estado del arte en la resolución de dichos problemas. [ 35 ]

Organizaciones

Véase también

Referencias

  1. ↑ Butler, RW (2001-08-06). "¿Qué son los métodos formales?" . Recuperado el 2006-11-16 .
  2. ↑ Holloway, C. Michael. "Por qué los ingenieros deberían considerar los métodos formales" (PDF) . 16.ª Conferencia de Sistemas de Aviónica Digital (27-30 de octubre de 1997). Archivado del original (PDF) el 16 de noviembre de 2006. Consultado el 16 de noviembre de 2006 .{{cite journal}}: Para citar una revista se requiere |journal=( ayuda )
  3. ↑ Monin, págs. 3-4
  4. ↑ Utting, Mark; Reeves, Steve (31 de agosto de 2001). "Enseñanza de métodos formales simplificados mediante pruebas" . Software Testing, Verification and Reliability . 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), Backus Normal Form vs Backus Naur Form. Communications of the ACM , 7(12):735–736.
  7. ↑ O'Hearn, Peter W.; Tennent, Robert D. (1997). Lenguajes tipo 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. ↑ Gleirscher, Mario; Marmsoler, Diego (noviembre de 2020). "Métodos formales en ingeniería de sistemas confiables: una encuesta a profesionales de Europa y Norteamérica" . Ingeniería de software empírica . 25 (6): 4473– 4546. arXiv : 1812.08815 . doi : 10.1007/s10664-020-09836-5 . ISSN 1573-7616 . Recuperado el 16 de mayo de 2026 . 
  10. ↑ A. Cortesi y M. Zanioli, Operadores de ampliación y reducción para la interpretación abstracta . Archivado el 23 de septiembre de 2015 en Wayback Machine . Computer Languages, Systems and Structures. Volumen 37(1), pp. 24–42, Elsevier, ISSN 1477-8424 (2011). 
  11. ↑ Bjørner, Dines; Henson, Martin C. (2008). Lógicas de los lenguajes de especificación . págs. VII– XI. 
  12. ↑ Bryant, Randal E. (2018). "Diagramas de decisión binarios". En Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.). Manual de verificación de modelos . pág. 191. 
  13. ↑ 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. 
  14. ↑ Prasad, Mukul R; Biere, Armin; Gupta, Aarti (25 de enero de 2005). "Una revisión de los avances recientes en la verificación formal basada en SAT". International Journal on Software Tools for Technology Transfer . 7 (2): 156– 173. doi : 10.1007/s10009-004-0183-4 .
  15. ^ 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 . 
  16. ↑ 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 . 
  17. ↑ Gheorghe, AV, & Ancel, E. (2008, noviembre). Integración de sistemas aéreos no tripulados en el Sistema Nacional del Espacio Aéreo. En Infrastructure Systems and Services: Building Networks for a Brighter Future (INFRA), 2008 First International Conference on (pp. 1-5). IEEE.
  18. ↑ Resolución y detección de conflictos coordinados aerotransportados, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/ Archivado el 5 de marzo de 2016 en Wayback Machine
  19. ↑ "Atelier B" . www.atelierb.eu .
  20. ↑ 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.
  21. ↑ 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.
  22. ↑ 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.
  23. ↑ E. Seligman, I. Yarom, " Métodos más conocidos para usar Cadence Conformal LEC ", en Intel.
  24. ↑ C. Eisner, A. Nahir, K. Yorav, " Verificación funcional de diseños con control de potencia mediante razonamiento composicional "", Verificación asistida por computadora, Springer Berlin Heidelberg, págs. 433–445.
  25. ↑ PC Attie, H. Chockler, " Verificación automática de emulaciones de registros tolerantes a fallos ", Electronic Notes in Theoretical Computer Science, vol. 149, n.º 1, págs. 49–60.
  26. ↑ KD Schubert, W. Roesner, JM Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, " Verificación funcional de los sistemas de microprocesador y multiprocesador IBM POWER7 ", IBM Journal of Research and Development, vol. 55, n.º 3.
  27. ↑ X2R-2, entregable D5.1 .
  28. ↑ Daniel Jackson y Jeannette Wing , "Métodos formales ligeros" , IEEE Computer , abril de 1996
  29. ↑ Vinu George y Rayford Vaughn, "Aplicación de métodos formales ligeros en la ingeniería de requisitos", archivado el 1 de marzo de 2006 en Wayback Machine , Crosstalk: The Journal of Defense Software Engineering , enero de 2003.
  30. ↑ Daniel Jackson, "Alloy: A Lightweight Object Modelling Notation" , ACM Transactions on Software Engineering and Methodology (TOSEM) , Volumen 11, Número 2 (abril de 2002), págs. 256-290
  31. ↑ Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality , Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6.
  32. ↑ 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.
  33. ↑ "ESBMC" . esbmc.org .
  34. ↑ "FizzBee" . fizzbee.io .
  35. ↑ 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 visión general de las competiciones en métodos formales". En Beyer, Dirk; Huisman, Marieke; Kordon, Fabrice; Steffen, Bernhard (eds.). Herramientas y algoritmos para la construcción y el análisis de sistemas . Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 3–24 . doi : 10.1007/978-3-030-17502-3_1 . ISBN  978-3-030-17502-3.
  36. ↑ 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 . hdl : 10138/335114 . ISSN 0004-3702 . 
  37. ↑ Cornejo, César (27 de enero de 2021). "Soporte aritmético basado en SAT para Alloy" . 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.
  38. ↑ Barrett, Clark; Deters, Morgan; de Moura, Leonardo; Oliveras, Albert; Stump, Aaron (1 de marzo de 2013). "6 años de SMT-COMP" . Journal of Automated Reasoning . 50 (3): 243–277 . doi : 10.1007/s10817-012-9246-5 . ISSN 1573-0670 . 
  39. ↑ Fedyukovich, Grigory; Rümmer, Philipp (13 de septiembre de 2021). "Informe de la competición: 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 . 
  40. ↑ Shukla, Ankit; Biere, Armin; Pulina, Luca; Seidl, Martina (noviembre de 2019). «Un estudio sobre las aplicaciones de las fórmulas booleanas cuantificadas». 2019 IEEE 31.ª Conferencia Internacional sobre Herramientas con Inteligencia Artificial (ICTAI) . IEEE. págs. 78–84 . doi : 10.1109/ICTAI.2019.00020 . ISBN  978-1-7281-3798-8.
  41. ↑ Pulina, Luca; Seidl, Martina (1 de septiembre de 2019). «Las evaluaciones de solucionadores QBF 2016 y 2017 (QBFEVAL'16 y QBFEVAL'17)» . Inteligencia artificial . 274 : 224– 248. doi : 10.1016/j.artint.2019.04.002 . ISSN 0004-3702 . 
  42. ↑ Beyer, Dirk (2022). "Avances en la verificación de software: SV-COMP 2022". En Fisman, Dana; Rosu, Grigore (eds.). Herramientas y algoritmos para la construcción y el análisis de sistemas . Lecture Notes in Computer Science. Vol. 13244. Cham: Springer International Publishing. pp. 375–402 . doi : 10.1007/978-3-030-99527-0_20 . ISBN   978-3-030-99527-0.
  43. ↑ Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2017-11-28). "SyGuS-Comp 2017: Resultados y análisis" . Actas electrónicas en ciencias de la computación teórica . 260 : 97–115 . arXiv : 1611.07627 . doi : 10.4204/EPTCS.260.9 . ISSN 2075-2180 . 

Lecturas adicionales

  • Jonathan P. Bowen y Michael G. Hinchey, Métodos formales . En Allen B. Tucker, Jr. (ed.), Manual de informática , 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 . 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) . Lecture Notes in Computer Science (LNCS). Vol.  12327. Springer . págs. 3–69 . doi : 10.1007/978-3-030-58298-2_1 . ISBN  978-3-030-58297-5. S2CID 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 Norteamérica" . 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