La verificación en tiempo de ejecución es un enfoque de análisis y ejecución de un sistema informático basado en la extracción de información de un sistema en ejecución y su uso para detectar y posiblemente reaccionar a los comportamientos observados que satisfacen o violan ciertas propiedades. [1] Por lo general, se desea que todos los sistemas satisfagan algunas propiedades muy particulares, como la velocidad de datos y la libertad de interbloqueo, y es posible que se implementen mejor algorítmicamente. Otras propiedades se pueden capturar más convenientemente como especificaciones formales . Las especificaciones de verificación en tiempo de ejecución se expresan típicamente en formalismos de predicados de seguimiento, como máquinas de estados finitos , expresiones regulares, patrones libres de contexto, lógicas temporales lineales, etc., o extensiones de estos. Esto permite un enfoque menos ad-hoc que las pruebas normales. Sin embargo, cualquier mecanismo para monitorear un sistema en ejecución se considera verificación en tiempo de ejecución, incluida la verificación contra oráculos de prueba e implementaciones de referencia [ cita requerida ] . Cuando se proporcionan especificaciones de requisitos formales, los monitores se sintetizan a partir de ellos y se infunden dentro del sistema por medio de instrumentación. La verificación en tiempo de ejecución se puede utilizar para muchos propósitos, como el monitoreo de políticas de seguridad o protección, depuración, prueba, verificación, validación, elaboración de perfiles, protección contra fallas, modificación de comportamiento (por ejemplo, recuperación), etc. La verificación en tiempo de ejecución evita la complejidad de las técnicas tradicionales de verificación formal , como la verificación de modelos y la demostración de teoremas, analizando solo uno o algunos rastros de ejecución y trabajando directamente con el sistema real, escalando así relativamente bien y dando más confianza en los resultados del análisis (porque evita el tedioso y el error (paso propenso a modelar formalmente el sistema), a expensas de una menor cobertura. Además, a través de sus capacidades de reflexión, la verificación en tiempo de ejecución puede convertirse en una parte integral del sistema de destino, monitoreando y guiando su ejecución durante la implementación.
Historia y contexto
La verificación de propiedades especificadas formal o informalmente frente a sistemas o programas en ejecución es un tema antiguo (ejemplos notables son la escritura dinámica en software, o dispositivos a prueba de fallas o temporizadores de vigilancia en hardware), cuyas raíces precisas son difíciles de identificar. La terminología de verificación en tiempo de ejecución se introdujo formalmente como el nombre de un taller de 2001 [2] destinado a abordar los problemas en el límite entre la verificación formal y las pruebas. Para bases de código grandes, la escritura manual de casos de prueba requiere mucho tiempo. Además, no todos los errores se pueden detectar durante el desarrollo. Klaus Havelund y Grigore Rosu han realizado las primeras contribuciones para automatizar la verificación en el Centro de Investigación Ames de la NASA para archivar altos estándares de seguridad en naves espaciales, rovers y tecnología de aviónica. [3] Propusieron una herramienta para verificar especificaciones en lógica temporal y para detectar condiciones de carrera y puntos muertos en programas Java mediante el análisis de rutas de ejecución únicas.
Actualmente, las técnicas de verificación del tiempo de ejecución a menudo se presentan con varios nombres alternativos, como monitoreo del tiempo de ejecución, verificación del tiempo de ejecución, reflexión del tiempo de ejecución, análisis del tiempo de ejecución, análisis dinámico , análisis simbólico dinámico / en tiempo de ejecución, análisis de trazas, análisis de archivos de registro, etc., todos referidos a instancias del mismo concepto de alto nivel aplicado a diferentes áreas o por académicos de diferentes comunidades. La verificación en tiempo de ejecución está íntimamente relacionada con otras áreas bien establecidas, como las pruebas (particularmente las pruebas basadas en modelos) cuando se usan antes de la implementación y los sistemas tolerantes a fallas cuando se usan durante la implementación.
Dentro de la amplia área de verificación en tiempo de ejecución, se pueden distinguir varias categorías, como:
- Monitoreo "sin especificación" que apunta a un conjunto fijo de propiedades principalmente relacionadas con la simultaneidad, como la atomicidad. El trabajo pionero en esta área es de Savage et al. con el algoritmo Eraser [4]
- seguimiento con respecto a las especificaciones lógicas temporales; Lee, Kannan y sus colaboradores, [5] [6] y Havelund y Rosu, han realizado contribuciones tempranas en esta dirección . [7] [8]
Enfoques básicos
El amplio campo de los métodos de verificación en tiempo de ejecución se puede clasificar en tres dimensiones: [9]
- El sistema se puede monitorear durante la ejecución en sí (en línea) o después de la ejecución, por ejemplo, en forma de análisis de registro (fuera de línea).
- El código de verificación está integrado en el sistema (como se hace en Programación orientada a aspectos ) o se proporciona como una entidad externa.
- El monitor puede informar la violación o validación de la especificación deseada.
Sin embargo, el proceso básico de verificación en tiempo de ejecución sigue siendo similar: [9]
- Un monitor se crea a partir de alguna especificación formal. Este proceso normalmente se puede hacer automáticamente si hay un autómata equivalente para el lenguaje formal de la propiedad se especifica en Para transformar una. Expresión regular una máquina de estados finitos se puede utilizar; una propiedad en lógica temporal lineal se puede transformar en un autómata Büchi (ver también Lógica temporal lineal para autómata Büchi ).
- El sistema está instrumentado para enviar eventos relacionados con su estado de ejecución al monitor.
- El sistema se ejecuta y es verificado por el monitor.
- El monitor verifica el seguimiento de eventos recibido y produce un veredicto si se cumple la especificación. Además, el monitor envía comentarios al sistema para corregir posibles comportamientos falsos. Cuando se usa el monitoreo fuera de línea, el sistema de causa no puede recibir retroalimentación, ya que la verificación se realiza en un momento posterior.
Ejemplos de
Los ejemplos siguientes discuten algunas propiedades simples que han sido consideradas, posiblemente con pequeñas variaciones, por varios grupos de verificación en tiempo de ejecución en el momento de escribir este artículo (abril de 2011). Para hacerlas más interesantes, cada propiedad a continuación utiliza un formalismo de especificación diferente y todas son paramétricas. Las propiedades paramétricas son propiedades sobre trazas formadas con eventos paramétricos, que son eventos que unen datos a parámetros. Aquí una propiedad paramétrica tiene la forma, dónde es una especificación en algún formalismo apropiado que se refiere a eventos paramétricos genéricos (no autenticados). La intuición de tales propiedades paramétricas es que la propiedad expresada pordebe mantenerse para todas las instancias de parámetros encontradas (a través de eventos paramétricos) en la traza observada. Ninguno de los siguientes ejemplos es específico de ningún sistema de verificación en tiempo de ejecución en particular, aunque obviamente se necesita soporte para parámetros. En los siguientes ejemplos se asume la sintaxis de Java, por lo que "==" es igualdad lógica, mientras que "=" es asignación. Algunos métodos (por ejemplo, update()
en UnsafeEnumExample) son métodos ficticios, que no forman parte de la API de Java, que se utilizan para mayor claridad.
HasNext
La interfaz Java Iterator requiere que hasNext()
se llame al método y devuelva verdadero antes de next()
que se llame al método. Si esto no ocurre, es muy posible que un usuario repita "al final" de una Colección . La figura de la derecha muestra una máquina de estados finitos que define un posible monitor para verificar y hacer cumplir esta propiedad con verificación en tiempo de ejecución. Desde el estado desconocido , siempre es un error llamar al next()
método porque tal operación podría ser insegura. Si hasNext()
se llama y devuelve verdadero , es seguro llamar next()
, por lo que el monitor entra en el estado más . Sin embargo, si el hasNext()
método devuelve falso , no hay más elementos y el monitor entra en el estado ninguno . En los estados more y none , llamar al hasNext()
método no proporciona información nueva. Es seguro llamar al next()
método desde el estado más , pero se desconoce si existen más elementos, por lo que el monitor vuelve a entrar en el estado desconocido inicial . Finalmente, llamar al next()
método desde el estado none da como resultado que se ingrese al estado de error . Lo que sigue es una representación de esta propiedad usando lógica temporal lineal paramétrica del tiempo pasado .
Esta fórmula dice que cualquier llamada al next()
método debe ser precedida inmediatamente por una llamada al hasNext()
método que devuelva verdadero. La propiedad aquí es paramétrica en el iterador i
. Conceptualmente, esto significa que habrá una copia del monitor para cada posible Iterador en un programa de prueba, aunque los sistemas de verificación en tiempo de ejecución no necesitan implementar sus monitores paramétricos de esta manera. El monitor de esta propiedad se establecería para activar un controlador cuando se viola la fórmula (de manera equivalente cuando la máquina de estados finitos entra en el estado de error ), lo que ocurrirá cuando next()
se llame sin llamar primero hasNext()
, o cuando hasNext()
se llame antes next()
, pero devuelva falso .
UnsafeEnum
La clase Vector en Java tiene dos medios para iterar sobre sus elementos. Se puede usar la interfaz Iterator, como se vio en el ejemplo anterior, o se puede usar la interfaz Enumeration . Además de la adición de un método de eliminación para la interfaz Iterator, la principal diferencia es que Iterator "falla rápidamente" mientras que Enumeration no lo es. Lo que esto significa es que si uno modifica el Vector (que no sea mediante el método de eliminación de Iterator) cuando se está iterando sobre el Vector usando un Iterator, se lanza una ConcurrentModificationException . Sin embargo, cuando se usa una enumeración, este no es un caso, como se mencionó. Esto puede resultar en resultados no deterministas de un programa porque el Vector se deja en un estado inconsistente desde la perspectiva de la Enumeración. Para los programas heredados que todavía usan la interfaz de Enumeración, es posible que desee hacer cumplir que las Enumeraciones no se usan cuando se modifica su Vector subyacente. El siguiente patrón regular paramétrico se puede utilizar para imponer este comportamiento:
Este patrón es paramétrico tanto en la enumeración como en el vector. Intuitivamente, y como los sistemas de verificación en tiempo de ejecución anteriores no necesitan implementar sus monitores paramétricos de esta manera, uno puede pensar en el monitor paramétrico para esta propiedad como la creación y el seguimiento de una instancia de monitor no paramétrica para cada posible par de Vector y Enumeración. Algunos eventos pueden afectar a varios monitores al mismo tiempo, por ejemplo v.update()
, por lo que el sistema de verificación en tiempo de ejecución debe (nuevamente conceptualmente) enviarlos a todos los monitores interesados. Aquí se especifica la propiedad para que indique los malos comportamientos del programa. Esta propiedad, entonces, debe ser monitoreada para la coincidencia del patrón. La figura de la derecha muestra el código Java que coincide con este patrón, violando así la propiedad. El vector, v, se actualiza después de que se crea la enumeración, e, y luego se usa e.
Cerradura de seguridad
Los dos ejemplos anteriores muestran propiedades de estado finito, pero las propiedades utilizadas en la verificación en tiempo de ejecución pueden ser mucho más complejas. La propiedad SafeLock aplica la política de que el número de adquisiciones y liberaciones de una clase de bloqueo (reentrante) coincida con una llamada de método determinada. Esto, por supuesto, no permite la liberación de bloqueos en métodos distintos a los que los adquieren, pero es muy posible que este sea un objetivo deseable para que lo logre el sistema probado. A continuación se muestra una especificación de esta propiedad utilizando un patrón paramétrico libre de contexto:
El patrón especifica secuencias equilibradas de pares de inicio / fin y adquisición / liberación anidados para cada hilo y bloqueo (es la secuencia vacía). Aquí, el comienzo y el final se refieren al comienzo y al final de cada método del programa (excepto las llamadas para adquirir y liberar ellos mismos). Son paramétricos en el Thread porque es necesario asociar el principio y el final de los métodos si y solo si pertenecen al mismo Thread. Los eventos de adquisición y liberación también son paramétricos en el Thread por la misma razón. Son, además, paramétricos en Lock porque no deseamos asociar los lanzamientos de un Lock con las adquisiciones de otro. En el extremo, es posible que haya una instancia de la propiedad, es decir, una copia del mecanismo de análisis sin contexto, para cada combinación posible de Thread con Lock; esto sucede, nuevamente, de manera intuitiva, porque los sistemas de verificación en tiempo de ejecución pueden implementar la misma funcionalidad de manera diferente. Por ejemplo, si un sistema tiene subprocesos, , y con cerraduras y , entonces es posible tener que mantener instancias de propiedad para los pares <,>, <,>, <,>, <,>, <,> y <,>. Esta propiedad debe ser monitoreada para detectar fallas para coincidir con el patrón porque el patrón especificó el comportamiento correcto. La figura de la derecha muestra un rastro que produce dos violaciones de esta propiedad. Los pasos hacia abajo en la figura representan el comienzo de un método, mientras que los pasos hacia arriba son el final. Las flechas grises de la figura muestran la correspondencia entre las adquisiciones y las liberaciones dadas de la misma cerradura. Para simplificar, la traza muestra solo un hilo y un candado.
Retos y aplicaciones de la investigación
La mayor parte de la investigación de verificación en tiempo de ejecución aborda uno o más de los temas que se enumeran a continuación.
Reducir la sobrecarga del tiempo de ejecución
La observación de un sistema en ejecución generalmente implica una sobrecarga de tiempo de ejecución (los monitores de hardware pueden hacer una excepción). Es importante reducir la sobrecarga de las herramientas de verificación en tiempo de ejecución tanto como sea posible, particularmente cuando los monitores generados se implementan con el sistema. Las técnicas de reducción de gastos generales en tiempo de ejecución incluyen:
- Instrumentación mejorada . Extraer eventos del sistema en ejecución y enviarlos a los monitores puede generar una gran sobrecarga de tiempo de ejecución si se hace de manera ingenua. Una buena instrumentación del sistema es fundamental para cualquier herramienta de verificación en tiempo de ejecución, a menos que la herramienta se dirija explícitamente a los registros de ejecución existentes. Hay muchos enfoques de instrumentación en uso actual, cada uno con sus ventajas y desventajas, que van desde la instrumentación personalizada o manual, a las bibliotecas especializadas, la compilación en lenguajes orientados a aspectos, el aumento de la máquina virtual y la creación de soporte de hardware.
- Combinación con análisis estático . Unacombinacióncomún [ cita requerida ] de análisis estáticos y dinámicos, que se encuentra particularmente en los compiladores, es monitorear todos los requisitos que no se pueden descargar estáticamente. Un enfoque dual y, en última instancia, equivalente tiende a convertirse en la norma [ cita requerida ] en la verificación en tiempo de ejecución, es decir, el uso de análisis estático para reducir la cantidad de monitoreo que de otro modo sería exhaustivo. El análisis estático se puede realizar tanto en la propiedad a monitorear como en el sistema a monitorear. El análisis estático de la propiedad a monitorear puede revelar que ciertos eventos son innecesarios para monitorear, que la creación de ciertos monitores puede retrasarse y que ciertos monitores existentes nunca se activarán y, por lo tanto, pueden recolectarse basura. El análisis estático del sistema a monitorear puede detectar código que nunca podrá influir en los monitores. Por ejemplo, al monitorear lapropiedad HasNext anterior, no es necesario instrumentar partes de código donde cada llamada
i.next()
es precedida inmediatamente en cualquier ruta por una llamadai.hasnext()
que devuelve verdadero (visible en el gráfico de flujo de control). - Generación y gestión eficiente de monitores . Al monitorear propiedades paramétricas como las de los ejemplos anteriores, el sistema de monitoreo necesita realizar un seguimiento del estado de la propiedad monitoreada con respecto a cada instancia de parámetro. El número de estos casos es teóricamente ilimitado y tiende a ser enorme en la práctica. Un desafío de investigación importante es cómo distribuir de manera eficiente los eventos observados precisamente a aquellas instancias que los necesitan. Un desafío relacionado es cómo mantener pequeño el número de tales instancias (para que el despacho sea más rápido), o en otras palabras, cómo evitar la creación de instancias innecesarias durante el mayor tiempo posible y, doblemente, cómo eliminar instancias ya creadas tan pronto como sea posible. se vuelven innecesarios. Finalmente, los algoritmos de monitoreo paramétrico generalmente generalizan algoritmos similares para generar monitores no paramétricos. Por tanto, la calidad de los monitores no paramétricos generados dicta la calidad de los monitores paramétricos resultantes. Sin embargo, a diferencia de otros enfoques de verificación (por ejemplo, verificación de modelos), el número de estados o el tamaño del monitor generado es menos importante en la verificación en tiempo de ejecución; de hecho, algunos monitores pueden tener un número infinito de estados, como el de lapropiedad SafeLock anterior, aunque en cualquier momento solo puede haber ocurrido un número finito de estados. Lo importante es la eficiencia con la que el monitor pasa de un estado al siguiente cuando recibe un evento del sistema en ejecución.
Especificando propiedades
Uno de los principales impedimentos prácticos de todos los enfoques formales es que sus usuarios son reacios a, o no saben, y no quieren aprender a leer o escribir especificaciones. En algunos casos, las especificaciones son implícitas, como las de interbloqueos y carreras de datos, pero en la mayoría de los casos es necesario generarlas. Un inconveniente adicional, particularmente en el contexto de la verificación en tiempo de ejecución, es que muchos lenguajes de especificación existentes no son lo suficientemente expresivos para capturar las propiedades deseadas.
- Mejores formalismos. Se ha realizado una gran cantidad de trabajo en la comunidad de verificación en tiempo de ejecución para diseñar formalismos de especificación que se ajusten a los dominios de aplicación deseados para la verificación en tiempo de ejecución mejor que los formalismos de especificación convencionales. Algunos de estos consisten en cambios sintácticos leves o nulos en los formalismos convencionales, pero solo en cambios en su semántica (por ejemplo, traza finita versus semántica de traza infinita, etc.) y en su implementación (máquinas optimizadas de estados finitos en lugar de autómatas Büchi, etc.) .). Otros amplían los formalismos existentes con características que son susceptibles de verificación en tiempo de ejecución, pero que pueden no serlo fácilmente para otros enfoques de verificación, como agregar parámetros, como se ve en los ejemplos anteriores. Por último, existen formalismos de especificación que se han diseñado específicamente para la verificación en tiempo de ejecución, que intentan lograr lo mejor para este dominio y se preocupan poco por otros dominios de aplicación. Diseñar formalismos de especificación universalmente mejores o específicamente de dominio mejores para la verificación en tiempo de ejecución es y seguirá siendo uno de sus principales desafíos de investigación.
- Propiedades cuantitativas. En comparación con otros enfoques de verificación, la verificación en tiempo de ejecución puede operar sobre valores concretos de las variables de estado del sistema, lo que permite recopilar información estadística sobre la ejecución del programa y utilizar esta información para evaluar propiedades cuantitativas complejas. Se necesitan lenguajes de propiedad más expresivos que nos permitan utilizar plenamente esta capacidad.
- Mejores interfaces. Leer y escribir especificaciones de propiedades no es fácil para los no expertos. Incluso los expertos a menudo miran durante minutos fórmulas lógicas temporales relativamente pequeñas (particularmente cuando tienen operadores "hasta" anidados). Un área de investigación importante es desarrollar potentes interfaces de usuario para varios formalismos de especificación que permitan a los usuarios comprender, escribir y tal vez incluso visualizar propiedades más fácilmente.
- Especificaciones mineras. No importa qué soporte de herramientas esté disponible para ayudar a los usuarios a producir especificaciones, casi siempre estarán más complacidos de tener que escribir ninguna especificación, particularmente cuando son triviales. Afortunadamente, hay muchos programas que hacen un uso supuestamente correcto de las acciones / eventos sobre los que uno quiere tener propiedades. Si ese es el caso, entonces es concebible que a uno le gustaría hacer uso de esos programas correctos aprendiendo automáticamente de ellos las propiedades deseadas. Incluso si se espera que la calidad general de las especificaciones extraídas automáticamente sea menor que la de las especificaciones producidas manualmente, pueden servir como punto de partida para estas últimas o como base para herramientas de verificación automática del tiempo de ejecución destinadas específicamente a encontrar errores (donde un la especificación se convierte en falsos positivos o negativos, a menudo aceptables durante las pruebas).
Modelos de ejecución y análisis predictivo
La capacidad de un verificador en tiempo de ejecución para detectar errores depende estrictamente de su capacidad para analizar los rastros de ejecución. Cuando los monitores se implementan con el sistema, la instrumentación suele ser mínima y los seguimientos de ejecución son lo más simples posible para mantener baja la sobrecarga del tiempo de ejecución. Cuando se usa la verificación en tiempo de ejecución para las pruebas, uno puede permitirse instrumentaciones más completas que aumenten los eventos con información importante del sistema que los monitores pueden usar para construir y, por lo tanto, analizar modelos más refinados del sistema en ejecución. Por ejemplo, el aumento de eventos con información de reloj vectorial y con datos e información de flujo de control permite a los monitores construir un modelo causal del sistema en ejecución en el que la ejecución observada fue solo una instancia posible. Cualquier otra permutación de eventos que sea consistente con el modelo es una ejecución factible del sistema, que podría ocurrir bajo un entrelazado de subprocesos diferente. La detección de violaciones de propiedad en tales ejecuciones inferidas (al monitorearlas) hace que el monitor prediga errores que no ocurrieron en la ejecución observada, pero que pueden ocurrir en otra ejecución del mismo sistema. Un desafío de investigación importante es extraer modelos de los rastros de ejecución que comprenden tantos otros rastros de ejecución como sea posible.
Modificación de comportamiento
A diferencia de las pruebas o la verificación exhaustiva, la verificación en tiempo de ejecución promete permitir que el sistema se recupere de las violaciones detectadas, mediante la reconfiguración, micro-reinicios o mediante mecanismos de intervención más finos, a veces denominados sintonización o dirección. La implementación de estas técnicas dentro del riguroso marco de verificación en tiempo de ejecución da lugar a desafíos adicionales.
- Especificación de acciones. Es necesario especificar la modificación a realizar de una manera lo suficientemente abstracta que no requiera que el usuario conozca detalles de implementación irrelevantes. Además, es necesario especificar cuándo puede tener lugar dicha modificación para mantener la integridad del sistema.
- Razonamiento sobre los efectos de la intervención. Es importante saber que una intervención mejora la situación, o al menos no la empeora.
- Interfaces de acción. De manera similar a la instrumentación para el monitoreo, necesitamos habilitar el sistema para recibir invocaciones de acciones. Los mecanismos de invocación dependerán necesariamente de los detalles de implementación del sistema. Sin embargo, a nivel de especificación, necesitamos proporcionar al usuario una forma declarativa de proporcionar retroalimentación al sistema especificando qué acciones deben aplicarse, cuándo y bajo qué condiciones.
Trabajo relacionado
Programación Orientada a Aspectos
Los investigadores de Runtime Verification reconocieron el potencial de utilizar la programación orientada a aspectos como técnica para definir la instrumentación de programas de forma modular. La programación orientada a aspectos (AOP) generalmente promueve la modularización de preocupaciones transversales. La verificación en tiempo de ejecución es naturalmente una de esas preocupaciones y, por lo tanto, puede beneficiarse de ciertas propiedades de AOP. Las definiciones de monitor orientadas a aspectos son en gran parte declarativas y, por lo tanto, tienden a ser más simples de razonar que la instrumentación expresada a través de una transformación de programa escrita en un lenguaje de programación imperativo. Además, los análisis estáticos pueden razonar sobre aspectos de seguimiento más fácilmente que sobre otras formas de instrumentación del programa, ya que toda la instrumentación está contenida en un solo aspecto. Muchas herramientas de verificación de tiempo de ejecución actuales se construyen, por lo tanto, en forma de compiladores de especificaciones, que toman una especificación expresiva de alto nivel como entrada y producen como código de salida escrito en algún lenguaje de programación orientado a aspectos (como AspectJ ).
Combinación con verificación formal
La verificación en tiempo de ejecución, si se usa en combinación con un código de recuperación comprobablemente correcto, puede proporcionar una infraestructura invaluable para la verificación del programa, que puede reducir significativamente la complejidad de este último. Por ejemplo, verificar formalmente el algoritmo de ordenación del montón es muy complicado. Una técnica menos desafiante para verificarlo es monitorear su salida para ser ordenada (un monitor de complejidad lineal) y, si no está ordenada, luego ordenarla usando algún procedimiento fácilmente verificable, digamos ordenación por inserción. El programa de clasificación resultante ahora es más fácilmente verificable, lo único que se requiere de heap-sort es que no destruya los elementos originales considerados como multiset, lo cual es mucho más fácil de probar. Mirando desde la otra dirección, se puede usar la verificación formal para reducir la sobrecarga de la verificación en tiempo de ejecución, como ya se mencionó anteriormente para el análisis estático en lugar de la verificación formal. De hecho, se puede comenzar con un programa completamente verificado en tiempo de ejecución, pero probablemente lento. Luego, se puede usar la verificación formal (o análisis estático) para descargar los monitores, de la misma manera que un compilador usa el análisis estático para descargar verificaciones en tiempo de ejecución de corrección de tipo o seguridad de la memoria .
Cobertura creciente
En comparación con los enfoques de verificación más tradicionales, una desventaja inmediata de la verificación en tiempo de ejecución es su cobertura reducida. Esto no es problemático cuando los monitores de tiempo de ejecución se implementan con el sistema (junto con el código de recuperación apropiado que se ejecutará cuando se infrinja la propiedad), pero puede limitar la efectividad de la verificación del tiempo de ejecución cuando se utiliza para encontrar errores en los sistemas. Las técnicas para aumentar la cobertura de la verificación en tiempo de ejecución con fines de detección de errores incluyen:
- Generación de entrada. Es bien sabido que generar un buen conjunto de entradas (valores de variables de entrada del programa, valores de llamadas al sistema, programas de subprocesos, etc.) puede aumentar enormemente la eficacia de las pruebas. Eso también es válido para la verificación en tiempo de ejecución utilizada para la detección de errores, pero además de usar el código del programa para impulsar el proceso de generación de entrada, en la verificación en tiempo de ejecución también se pueden usar las especificaciones de propiedad, cuando estén disponibles, y también se pueden usar técnicas de monitoreo para inducir comportamientos deseados. Este uso de la verificación en tiempo de ejecución hace que esté estrechamente relacionado con las pruebas basadas en modelos, aunque las especificaciones de verificación del tiempo de ejecución suelen ser de uso general, no necesariamente diseñadas por motivos de prueba. Considere, por ejemplo, que uno quiere probar lapropiedad UnsafeEnum de propósito general anterior. En lugar de simplemente generar el monitor mencionado anteriormente para observar pasivamente la ejecución del sistema, se puede generar un monitor más inteligente que congela el hilo que intenta generar el segundoevento e.nextElement () (justo antes de que lo genere), dejando que los otros hilos se ejecuten con la esperanza de que uno de ellos pueda generar unevento v.update () , en cuyo caso se ha encontrado un error.
- Ejecución simbólica dinámica. En ejecución simbólica, los programas se ejecutan y supervisan simbólicamente, es decir, sin entradas concretas. Una ejecución simbólica del sistema puede cubrir un gran conjunto de entradas concretas. Las técnicas de verificación de la satisfacción o la resolución de restricciones listas para usar se utilizan a menudo para impulsar ejecuciones simbólicas o para explorar sistemáticamente su espacio. Cuando los verificadores de satisfacibilidad subyacentes no pueden manejar un punto de elección, entonces se puede generar una entrada concreta para pasar ese punto; esta combinación de conc rete y symb olic ejecución también se conoce como ejecución concolic.
Ver también
Referencias
- ^ Ezio Bartocci e Yliès Falcone (eds), Lectures on Runtime Verification - Introductory and Advanced Topics, Parte de la serie de libros Lecture Notes in Computer Science (LNCS, volumen 10457), también parte de la subserie de libros Programming and Software Engineering (LNPSE, volumen 10457), 2018 . Apuntes de conferencias en Ciencias de la Computación. 10457 . 2018. doi : 10.1007 / 978-3-319-75632-5 . ISBN 978-3-319-75631-8.
- ^ "RV'01 - Primer taller sobre verificación en tiempo de ejecución" . Conferencias de verificación en tiempo de ejecución . 23 de julio de 2001 . Consultado el 25 de febrero de 2017 .
- ^ Klaus Havelund y Grigore Rosu. 2004. Una descripción general de la herramienta de verificación en tiempo de ejecución Java PathExplorer. Métodos formales en el diseño de sistemas, 24 (2), marzo de 2004.
- ^ Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro y Thomas Anderson. 1997. Eraser: un detector de carrera de datos dinámicos para programas multiproceso. ACM Trans. Computación. Syst. 15 (4), noviembre de 1997, págs. 391-411.
- ^ Moonjoo Kim, Mahesh Viswanathan, Insup Lee, Hanêne Ben-Abdellah, Sampath Kannan y Oleg Sokolsky, Monitoreo formalmente especificado de propiedades temporales, Actas de la Conferencia europea sobre sistemas en tiempo real, junio de 1999.
- ^ Insup Lee, Sampath Kannan, Moonjoo Kim, Oleg Sokolsky, Mahesh Viswanathan, Garantía de tiempo de ejecución basada en especificaciones formales, Actas de la Conferencia internacional sobre técnicas y aplicaciones de procesamiento paralelo y distribuido, junio de 1999.
- ^ Klaus Havelund, Uso del análisis en tiempo de ejecución para guiar la verificación del modelo de programas Java, 7mo taller internacional SPIN, agosto de 2000.
- ^ Klaus Havelund y Grigore Rosu, Programas de supervisión mediante reescritura, ingeniería de software automatizada (ASE'01), noviembre de 2001.
- ^ a b Yliès Falcone, Klaus Havelund y Giles, Un tutorial sobre la verificación en tiempo de ejecución, 2013