stringtranslate.com

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] El uso de métodos formales para el diseño de software y hardware está motivado por la expectativa de que, como en otras disciplinas de ingeniería, realizar un análisis matemático apropiado puede contribuir a la confiabilidad y robustez de un diseño. [2]

Los métodos formales emplean una variedad de fundamentos teóricos de la informática , incluidos cálculos lógicos , lenguajes formales , teoría de autómatas , teoría de control , semántica de programas , sistemas de tipos y teoría de tipos . [3]

Fondo

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

Taxonomía

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

Más información al respecto se amplía a continuación.

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

Métodos formales ligeros

Algunos profesionales creen que la comunidad de métodos formales ha puesto demasiado énfasis en la formalización total de una especificación o diseño. [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 total sea una tarea difícil y costosa. Como alternativa, se han propuesto varios métodos formales ligeros , que enfatizan la especificación parcial y la aplicación enfocada. Ejemplos de este enfoque ligero de los métodos formales incluyen la notación de modelado de objetos Alloy , [7] la síntesis de Denney de algunos aspectos de la notación Z con desarrollo impulsado por casos de uso , [8] y las herramientas CSK VDM . [9]

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 deseado. Esta descripción formal se puede utilizar para guiar futuras actividades de desarrollo (ver las siguientes secciones); Además, se puede utilizar para verificar que los requisitos del 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 definidas de forma precisa e inequívoca.

Durante años se ha observado la necesidad de sistemas de especificaciones formales. En el informe ALGOL 58 , [10] 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). [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 integrada de un proceso de desarrollo de sistemas respaldado por herramientas.

Una vez que se ha producido una especificación formal, la especificación puede usarse como 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:

Verificación

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

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

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. Una herramienta de este tipo puede sustituir los métodos de verificación tradicionales (la herramienta puede incluso estar certificada).

Prueba dirigida por humanos

A veces, la motivación para demostrar la corrección de un sistema no es la necesidad obvia de asegurarse de la corrección del sistema, sino el deseo de comprender mejor el sistema. En consecuencia, algunas pruebas de corrección se producen al estilo de la prueba matemática : escritas a mano (o tipografiadas) utilizando lenguaje natural , utilizando un nivel de informalidad común a tales pruebas. Una "buena" prueba es aquella que es legible y comprensible para otros lectores humanos.

Los críticos de tales enfoques señalan que la ambigüedad inherente al lenguaje natural permite que no se detecten errores en tales pruebas; A menudo, pueden estar presentes errores sutiles en los detalles de bajo nivel que normalmente pasan por alto tales pruebas. Además, el trabajo involucrado en producir una prueba tan buena requiere un alto nivel de sofisticación y experiencia matemática.

Prueba automatizada

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

Algunos demostradores de teoremas automatizados requieren orientación sobre qué propiedades son lo suficientemente "interesantes" como para seguirlas, mientras que otros funcionan sin intervención humana. Los verificadores de modelos pueden rápidamente atascarse en la verificación de millones de estados poco interesantes si no se les proporciona un modelo suficientemente abstracto.

Los defensores de tales sistemas argumentan que los resultados tienen mayor certeza matemática que las pruebas producidas por humanos, ya que todos los tediosos detalles han sido verificados algorítmicamente. La formación necesaria para utilizar dichos sistemas también es inferior a la necesaria para producir buenas demostraciones matemáticas a mano, lo que hace que las técnicas sean accesibles a una variedad más amplia de profesionales.

Los críticos señalan que algunos de esos sistemas son como oráculos : hacen un pronunciamiento de la verdad, pero no dan explicación de esa verdad. También está el problema de " verificar al verificador "; Si el programa que ayuda en la verificación no está probado, puede haber motivos para dudar de la solidez de los resultados obtenidos. Algunas herramientas modernas de verificación de modelos producen un "registro de prueba" que detalla cada paso de su prueba, lo que permite realizar, con las herramientas adecuadas, una verificación independiente.

La característica principal del enfoque de interpretación abstracta es que proporciona un análisis sólido, es decir, que no arroja falsos negativos. Además, es escalable de manera eficiente, al ajustar el dominio abstracto que representa la propiedad a analizar y al aplicar operadores de ampliación [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 de sistemas operativos como seL4 . Existen varios ejemplos en los que se han utilizado para verificar la funcionalidad del hardware y software utilizado en los centros de datos . IBM utilizó ACL2 , un demostrador de teoremas, en el proceso de desarrollo del procesador AMD x86. [ cita necesaria ] Intel utiliza estos métodos para verificar su hardware y firmware (software permanente programado en una memoria de solo lectura ) [ cita necesaria ] . El Dansk Datamatik Center utilizó métodos formales en la década de 1980 para desarrollar un sistema compilador para el lenguaje de programación Ada que se convirtió en un producto comercial de larga duración. [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 Nacional del Espacio Aéreo, [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 metros instalados en todo el mundo por Alstom y Siemens , y también para la certificación Common Criteria y el desarrollo de modelos de sistemas por parte de ATMEL y STMicroelectronics .

La mayoría de los proveedores de hardware conocidos, como IBM, Intel y AMD, han utilizado con frecuencia la verificación formal en el hardware. Hay muchas áreas de hardware en las que Intel ha utilizado métodos formales para verificar el funcionamiento de los productos, como la verificación parametrizada del protocolo coherente de caché, [18] la validación del motor de ejecución del procesador Intel Core i7 [19] (mediante demostración de teoremas, BDD , y evaluación simbólica), optimización para la arquitectura Intel IA-64 utilizando el probador del teorema de la luz HOL, [20] y verificación del controlador Gigabit Ethernet de doble puerto de alto rendimiento con soporte para el protocolo PCI express y la tecnología de gestión avanzada de Intel utilizando Cadence. [21] De manera similar, IBM ha utilizado métodos formales en la verificación de puertas de alimentación, [22] registros, [23] y verificación funcional del microprocesador IBM Power7. [24]

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, especificaciones y diseño. Es más probable que los métodos formales se apliquen a software y sistemas críticos para la seguridad, como el software de aviónica . Los estándares de garantía de seguridad del software, como DO-178C, permiten el uso de métodos formales mediante complementación, y Common Criteria exige métodos formales en los niveles más altos de categorización.

Para el software secuencial, los ejemplos de métodos formales incluyen el método B , los lenguajes de especificación utilizados en la demostración automatizada de teoremas , RAISE y la notación Z.

En programación funcional , las pruebas basadas en propiedades han permitido la especificación matemática y las pruebas (si no exhaustivas) del comportamiento esperado de funciones individuales.

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

Para software y sistemas concurrentes, las redes de Petri , el álgebra de procesos y las máquinas de estados finitos (que se basan en la teoría de los autómatas ; ver también máquina virtual de estados finitos o máquina de estados finitos impulsada por eventos ) permiten especificaciones de software ejecutables y pueden usarse para construir y validar. comportamiento de la aplicación.

Otro enfoque de los métodos formales en el desarrollo de software es escribir una especificación en alguna forma de lógica (generalmente una variación de la lógica de primer orden ) y luego ejecutar directamente la lógica como si fuera un programa. El lenguaje OWL , basado en la lógica de descripción , es un ejemplo. También se está trabajando en mapear alguna versión del inglés (u otro lenguaje natural) automáticamente hacia y desde la lógica, así como en ejecutar la lógica directamente. Ejemplos de ello son Attempto Controlled English e Internet Business Logic, que no buscan controlar el vocabulario ni la sintaxis. Una característica de los sistemas que admiten el mapeo bidireccional inglés-lógico y la ejecución directa de la lógica es que se les puede hacer explicar sus resultados, en inglés, a nivel empresarial o científico. [ cita necesaria ]

Métodos formales y notaciones.

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

Idiomas de especificación

damas modelo

Solucionadores y competiciones.

Muchos problemas en los métodos formales son NP-difíciles , pero pueden resolverse en los casos que surgen en la práctica. Por ejemplo, el problema de satisfacibilidad booleano es NP-completo según el teorema de Cook-Levin , pero los solucionadores SAT pueden resolver una variedad de casos grandes. Hay "solucionadores" para una variedad de problemas que surgen en los métodos formales, y hay muchos concursos periódicos para evaluar los últimos avances en la resolución de dichos problemas. [26]

Organizaciones

Ver también

Referencias

  1. ^ Mayordomo, 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 a 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}}: Citar diario requiere |journal=( ayuda )
  3. ^ Monin, páginas 3-4
  4. ^ X2R-2, entregable D5.1 .
  5. ^ Daniel Jackson y Jeannette Wing , "Lightweight Formal Methods", IEEE Computer , abril de 1996
  6. ^ 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
  7. ^ Daniel Jackson, "Alloy: A Lightweight Object Modeling Notation", ACM Transactions on Software Engineering and Methodology (TOSEM) , volumen 11, número 2 (abril de 2002), págs.
  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, "A Lightweight Approach to Formal Methods" Archivado el 9 de marzo de 2006 en Wayback Machine , en las actas del taller internacional sobre tendencias actuales en métodos formales aplicados , Boppard, Alemania, Springer-Verlag, octubre de 1998
  10. ^ Backus, JW (1959). "La sintaxis y semántica del lenguaje algebraico internacional propuesto en la Conferencia ACM-GAMM de Zúrich". Actas de la Conferencia Internacional sobre Procesamiento de Información . UNESCO.
  11. ^ Knuth, Donald E. (1964), Forma normal de Backus frente a forma de Backus Naur. Comunicaciones de la ACM , 7(12):735–736.
  12. ^ A. Cortesi y M. Zanioli, Operadores de ampliación 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, 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.
  14. ^ Bjørner, cena; 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. (noviembre de 2008). Integración de sistemas aéreos no tripulados al Sistema Nacional del Espacio Aéreo. En Sistemas y servicios de infraestructura: construcción de 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 desde el aire, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/
  17. ^ "Taller 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ógica de orden superior, Springer Berlin Heidelberg, 2004, págs.
  21. ^ E. Seligman, I. Yarom, "Métodos más conocidos para utilizar Cadence Conformal LEC", en Intel.
  22. ^ C. Eisner, A. Nahir, K. Yorav, "Verificación funcional de diseños con control eléctrico mediante razonamiento compositivo [ enlace muerto permanente ] ", Verificación asistida por computadora, Springer Berlin Heidelberg, págs.
  23. ^ 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.
  24. ^ KD Schubert, W. Roesner, JM Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, "Verificación funcional del microprocesador IBM POWER7 y los sistemas multiprocesador POWER7", IBM Journal of Research and Development, vol. 55, nº 3.
  25. ^ "ESBMC". esbmc.org .
  26. ^ Bartocci, Ezio; Beyer, Dirk; Negro, Paul E.; Fedyukovich, Grigory; Garavel, Hubert; Hartmanns, Arnd; Huisman, Marieke; Cordón, Fabrice; Nagele, Julián; Sighireanu, Mihaela; Steffen, Bernhard; Suda, Martín; Sutcliffe, Geoff; Weber, Tjark; Yamada, Akihisa (2019). Beyer, Dirk; Huisman, Marieke; Cordón, Fabrice; Steffen, Bernhard (eds.). "TOOLympics 2019: una descripción general de las competiciones en métodos formales". Herramientas y Algoritmos para la Construcción y Análisis de Sistemas . Apuntes de conferencias sobre informática. Cham: Springer International Publishing: 3–24. doi : 10.1007/978-3-030-17502-3_1 . ISBN 978-3-030-17502-3.
  27. ^ 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.
  28. ^ 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.: Asociación de Maquinaria de Computación: 1161–1163. doi :10.1145/3324884.3415285. ISBN 978-1-4503-6768-4.
  29. ^ Barrett, Clark; Disuade, Morgan; de Moura, Leonardo; Oliveras, Alberto; Tocón, 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.
  30. ^ 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.
  31. ^ Shukla, Ankit; Biere, Armin; Pulina, Luca; Seidl, Martina (noviembre de 2019). "Una encuesta sobre aplicaciones de fórmulas booleanas cuantificadas". IEEE: 78–84. doi :10.1109/ICTAI.2019.00020. ISBN 978-1-7281-3798-8. {{cite journal}}: Citar diario requiere |journal=( ayuda )
  32. ^ 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.
  33. ^ Beyer, Dirk (2022). Fisman, Dana; Rosu, Grigore (eds.). "Avances en la verificación de software: SV-COMP 2022". Herramientas y Algoritmos para la Construcción y Análisis de Sistemas . Apuntes de conferencias sobre informática. Cham: Springer International Publishing: 375–402. doi : 10.1007/978-3-030-99527-0_20 . ISBN 978-3-030-99527-0.
  34. ^ Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (28-11-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.

Otras lecturas

enlaces externos

Material de archivo