Un objetivo importante de los métodos formales es demostrar la corrección de los sistemas, ya sea por medios automatizados o dirigidos por humanos. Sin embargo, parece que incluso si puede proporcionar una prueba de corrección, es posible que NO pueda garantizar que el sistema no falle. Por ejemplo:
- La especificación puede no modelar el sistema correctamente, o un sistema de producción puede ser demasiado complicado para modelar, o el sistema puede ser inherentemente defectuoso debido a requisitos contradictorios. ¿Qué técnicas se conocen para probar si una especificación tiene algún sentido?
- ¡El proceso de prueba también puede ser defectuoso! ¿Quién sabe que esas reglas de inferencia son correctas y legítimas? Además, las pruebas pueden ser muy grandes, y ¿cómo sabemos que no contienen errores? Este es el corazón de la crítica en "Procesos sociales y pruebas de teoremas y programas" de de Millo, Lipton y Perlis. ¿Cómo responden los investigadores de métodos formales modernos a esta crítica?
- En tiempo de ejecución, hay muchos eventos y factores no deterministas que pueden afectar seriamente el sistema. Por ejemplo, los rayos cósmicos pueden alterar la RAM de maneras impredecibles y, en general, no tenemos garantías de que el hardware no sufrirá fallas bizantinas, que Lamport ha demostrado que son muy difíciles de resistir. ¡Entonces la corrección del sistema estático no garantiza que el sistema no falle! ¿Hay alguna técnica conocida para explicar la falibilidad del hardware real?
- En la actualidad, las pruebas son la herramienta más importante que tenemos para establecer que el software funciona. Parece que debería ser una herramienta complementaria con métodos formales. Sin embargo, principalmente veo investigaciones que se centran en métodos formales o pruebas. ¿Qué se sabe sobre combinar los dos?
Respuestas:
En cuanto a 4: hay mucho trabajo combinando métodos formales y pruebas. Buscar en Google "pruebas de métodos formales" revela una gran cantidad de trabajo. Aunque hay muchos objetivos diferentes de dicho trabajo, uno de los objetivos clave es generar conjuntos de pruebas más efectivos. Esta charla ofrece una buena introducción, basada en la verificación del modelo.
También en relación con el problema de la seguridad del software , que se ha editado fuera de la cuestión: los métodos formales deben trabajar más duro para entregar en ese ámbito. Por lo general, uno escribe una especificación para una pieza de software y verifica que la especificación se cumple, es decir, que cuando la entrada satisface la condición previa de que la salida satisface la condición posterior. Para garantizar un software seguro, también es necesario verificar que el software se comporte con sensatez para la entrada que no cumpla con la condición previa. (Esto es, por supuesto, equivalente a establecer la condición previa como verdadera para todas las entradas). El espacio de todas las entradas suele ser mucho más grande que una entrada bien formada, pero generalmente es un lugar donde incluso el software funcionalmente correcto puede ser violado, simplemente por violando sus supuestos.
Con respecto al punto 3: se ha realizado algún trabajo para verificar los sistemas en entornos donde las fallas se modelan explícitamente, incluida la lógica de falla: razonamiento sobre programas tolerantes a fallas. Matthew Meola y David Walker. Simposio europeo sobre programación, 2010. El trabajo sobre la verificación del modelo probabilístico y la verificación probabilística ciertamente también abordan en cierta medida el problema de las fallas.
fuente
Sus puntos en orden:
fuente
Los métodos formales ya han demostrado que funcionan a lo grande. Sin ellos, no hubiéramos podido hacer frente a la complejidad del diseño de sistemas digitales modernos (microprocesadores).
Ningún microenvío sin tener su lógica sujeta a verificación de equivalencia funcional; sin que su FPU haya estado sujeta a FV; sin que sus protocolos de coherencia de caché hayan estado sujetos a FV (este ha sido el caso desde 1995).
Salvo las diferencias obvias entre el software y los sistemas físicos diseñados (por ejemplo, puentes, donde se pueden agregar factores de seguridad), desempeñan el papel de matemática de ingeniería en CS. Sin embargo, el uso de FM siempre depende del beneficio / costo. Las pruebas de Fuzz dan buenos resultados en compañías como Microsoft (Google SAGE en una sola diapositiva).
Incluso dentro de un micro, hay subsistemas (por ejemplo, tuberías de microprocesador), donde FV no ha tenido el mismo impacto que en otros lugares (por ejemplo, FPU, donde las pruebas convencionales no se realizaron en muchos casos cuando la evaluación formal de la trayectoria simbólica demostró la ausencia de errores : Kaivola et al CAV'09).
Los métodos formales también se están utilizando en la síntesis de artefactos (código, pruebas de alta calidad, cronogramas para el drenaje óptimo de los bancos de baterías, ...). Por supuesto, todas las cuestiones planteadas en la pregunta son bastante válidas y, como en cualquier otro uso de la tecnología, los anuncios falsos deben ser reconocidos y evitados.
fuente
Con respecto a 2: si el sistema se formaliza en un asistente de prueba (por ejemplo, Twelf o Agda o Coq) y se verifican las propiedades de solidez e integridad, y las pruebas se realizan en esta codificación, esto no es un problema. Es posible que haya formalizado un sistema que no describe lo que pretendía, pero al menos no tendrá pruebas incorrectas o un sistema roto en el que está razonando.
fuente
Sí, quizás no hay garantías . Los métodos formales están destinados a encontrar y eliminar errores y convencer a los humanos.
Puede que le interesen las herramientas de verificación de modelos para especificaciones de sistemas formales .
Creo que (debido al teorema de incompletitud de Goedel) mostrar que un sistema de reglas de inferencia es consistente necesariamente atrae a un conjunto aún más poderoso de reglas de inferencia.
Afortunadamente, un pequeño verificador de pruebas puede verificar las grandes pruebas que los humanos pueden leer y comprender en un tiempo razonable. Esto a veces se llama el "criterio de Bruijn". Si cree que el verificador de pruebas no certificará una prueba incorrecta, solo necesita verificar el verificador.
¿Qué tal un lenguaje ensamblador con tipo tolerante a fallas ?
"La conferencia TAP está dedicada a la convergencia de pruebas y pruebas" .
Simplemente buscar en Google "pruebas y pruebas" tiene varios buenos resultados por encima del pliegue.
fuente
Definitivamente es una decisión judicial. En ingeniería de software, las personas han diseñado una metodología muy estricta para encontrar / escribir / confirmar las especificaciones. Esto lo hacen los humanos reales y usan un proceso no formal (en el sentido no matemático), por lo que todavía está sujeto a inconsistencia, pero al final del día, corresponde a lo que la gente quiere verificar, ni más ni menos.
Claro, hay un campo de verificación conocido como verificación de tiempo de ejecución , también puede usar la verificación del modelo basado en la ejecución en el sistema real que se ejecuta en un entorno totalmente virtual sujeto a un escenario específico (contribuí a esto con V-DS + APMC ). Sin embargo, este es claramente un problema importante para agregar la interacción entre el sistema y el entorno en el proceso de verificación.
Wow, hoy seré totalmente desvergonzado y volveré a citarme. Con los coautores, trabajamos para combinar la verificación y prueba de modelos, puede consultar la lista de publicaciones de un antiguo estudiante de doctorado de nuestro grupo o buscar "verificación probabilística de modelo aproximada" o "verificación estadística de modelo" en cualquier buen motor de búsqueda (trabajo realizado por Younes et al., Sen et al. O yo mismo et al. Y muchos otros).
fuente
Puede que le interesen mucho los trabajos de John Rushby , uno de los diseñadores del probador de teoremas PVS, que está genéricamente interesado en exactamente los puntos que menciona. Es posible que le guste leer este informe clásico para la FAA sobre el uso de Métodos formales y la Certificación de sistemas críticos (1993) , y sus escritos más recientes sobre el montaje de un caso de seguridad probabilístico y formal a partir de varios medios de evidencia proporcionados (pruebas, pruebas, análisis, etc.)
fuente