Verificación en tiempo de ejecución
Runtime Verification Inc. es una empresa emergente destinada a utilizar técnicas basadas en la verificación en tiempo de ejecución para mejorar la seguridad, fiabilidad y corrección de los sistemas de software. Estamos fundados y atendidos por pioneros y líderes en el campo de la verificación en tiempo de ejecución, con más de 100 publicaciones y herramientas relacionadas que dieron forma al campo. Nuestra sede se encuentra en Champaign-Urbana, Illinois, a poca distancia del campus de la Universidad de Illinois. La verificación en tiempo de ejecución es un enfoque de análisis de software dinámico que analiza los programas a medida que se ejecutan, observando los resultados de la ejecución y utilizando esos resultados para encontrar errores. La verificación en tiempo de ejecución se basa en ciertas propiedades que la ejecución del programa no debe infringir. Algunas de estas propiedades, como la falta de carreras de datos en un programa simultáneo, son universales y se pueden comprobar automáticamente. Otras propiedades, como la especificación de una biblioteca propietaria, son personalizadas para una aplicación o propósito específico. La verificación en tiempo de ejecución puede comprobar las propiedades universales automáticamente, sin necesidad de entrada de desarrollo, y puede comprobar las propiedades personalizadas expresadas formalmente por los desarrolladores. La verificación en tiempo de ejecución puede ser más ligera que las técnicas de análisis formal tradicionales, como la comprobación de modelos o la verificación deductiva. Dado que la verificación en tiempo de ejecución solo tiene en cuenta la ejecución del sistema y no su código, es posible encontrar errores rigurosamente al escalar a grandes bases de código. La verificación en tiempo de ejecución también es más precisa que las técnicas de análisis estático ligero, que a menudo simplifican suposiciones o usan heurística imprecisa para analizar código, lo que conduce a falsos positivos que pueden frustrar a los desarrolladores y evaluadores. La verificación en tiempo de ejecución no está pensada para reemplazar las pruebas tradicionales basadas en unidades, funcionales e integración, ni incluso herramientas de análisis estático ligeras. Creemos que la verificación en tiempo de ejecución es un buen complemento para estas técnicas, proporcionando una alta confianza en la solidez del comportamiento de las aplicaciones tradicionalmente reservadas para técnicas de métodos formales complejos e inaccesibles, sin dejar de ser práctico sin escalar a grandes bases de código.
