Java Pathfinder

Java Pathfinder (JPF) es un sistema para verificar programas ejecutables de código de bytes Java . JPF fue desarrollado en el Centro de Investigación Ames de la NASA y se publicó como código abierto en 2005. El acrónimo JPF no debe confundirse con el proyecto Java Plugin Framework , que no guarda relación con este .

El núcleo de JPF es una máquina virtual Java . JPF ejecuta programas Java bytecode normales y puede almacenar, comparar y restaurar estados de programas. Su aplicación principal ha sido la verificación de modelos de programas concurrentes , para encontrar defectos como condiciones de carrera y bloqueos mutuos . Con sus respectivas extensiones, JPF también se puede utilizar para una variedad de otros propósitos, incluyendo:

• Verificación de modelos de aplicaciones distribuidas
• Verificación de modelos de interfaces de usuario
• generación de casos de prueba mediante ejecución simbólica
• inspección de programas de bajo nivel
• Instrumentación del programa y monitorización en tiempo de ejecución

JPF no tiene una noción fija de ramas en el espacio de estados y puede manejar tanto datos como opciones de planificación.

JPF es un sistema abierto que se puede extender de diversas maneras. Las principales construcciones de extensión son:

• oyentes : para implementar propiedades complejas (por ejemplo, propiedades temporales).
• Clases pares : para ejecutar código a nivel de la JVM del host (en lugar de JPF), que se utiliza principalmente para implementar métodos nativos.
• Fábricas de bytecode : para proporcionar semánticas de ejecución alternativas de las instrucciones de bytecode (por ejemplo, para implementar la ejecución simbólica).
• generadores de opciones : para implementar bifurcaciones en el espacio de estados, como opciones de programación o conjuntos de valores de datos.
• serializadores : para implementar abstracciones del estado del programa
• editores - para producir diferentes formatos de salida
• Políticas de búsqueda : utilizar diferentes algoritmos de recorrido del espacio de estados del programa.

JPF incluye un sistema de módulos en tiempo de ejecución para empaquetar dichas construcciones en proyectos de extensión JPF independientes . Varios de estos proyectos están disponibles en el servidor principal de JPF, incluyendo un modo de ejecución simbólica, análisis numérico, detección de condiciones de carrera para modelos de memoria relajados, verificación de modelos de interfaz de usuario y muchos más.

• JPF no puede analizar métodos nativos de Java . Si el sistema bajo prueba llama a dichos métodos, estos deben proporcionarse dentro de clases pares o ser interceptados por oyentes.
• Como verificador de modelos, JPF es susceptible a la explosión combinatoria , aunque realiza una reducción de orden parcial sobre la marcha.
• El sistema de configuración para los módulos JPF y las opciones de tiempo de ejecución puede ser complejo.

• MoonWalker : similar a Java PathFinder, pero para programas .NET en lugar de programas Java.

• Un nuevo software de la NASA detecta "errores" en el código informático Java.
• La NASA desarrolla un nuevo software para detectar "errores" en el código informático Java.

• Willem Visser, Corina S. Păsăreanu , Sarfraz Khurshid. Generación de entradas de prueba con Java PathFinder. En: George S. Avrunin, Gregg Rothermel (Eds.): Actas del Simposio Internacional ACM/SIGSOFT sobre Pruebas y Análisis de Software 2004. ACM Press, 2004. ISBN 1-58113-820-2.
• Willem Visser, Klaus Havelund, Guillaume Brat, Seungjoon Park, Flavio Lerda, Programas de verificación de modelos, Ingeniería de software automatizada 10(2), 2003.
• Klaus Havelund, Willem Visser, La verificación de modelos de programas como una nueva tendencia, STTT 4(1), 2002.
• Klaus Havelund, Thomas Pressburger, Model Checking Java Programs using Java PathFinder, STTT 2(4), 2000.