Java-следопыт

Java-следопыт
Разработчик(и)	НАСА
Стабильная версия	6.0 / 30 ноября 2010 г.
Написано в	Ява
Операционная система	Кросс-платформенный
Размер	1,6 МБ (в архиве)
Тип	проверки программного обеспечения Инструмент , виртуальная машина
Лицензия	Лицензия Apache версии 2
Веб-сайт	https://github.com/javapathfinder/

Java Pathfinder (JPF) — это система проверки исполняемых программ Java с байт-кодом . JPF был разработан в НАСА Исследовательском центре Эймса и открыт в 2005 году. Аббревиатуру JPF не следует путать с несвязанным проектом Java Plugin Framework .

Ядром JPF является виртуальная машина Java . JPF выполняет обычные программы с байт-кодом Java и может сохранять, сопоставлять и восстанавливать состояния программы. Его основным применением была проверка моделей параллельных программ для обнаружения дефектов, таких как гонки данных и взаимоблокировки . С соответствующими расширениями JPF также можно использовать для множества других целей, включая

проверка модели распределенных приложений
проверка моделей пользовательских интерфейсов
генерация тестовых примеров посредством символьного выполнения
проверка программы низкого уровня
инструментирование программы и мониторинг времени выполнения

JPF не имеет фиксированного понятия ветвей пространства состояний и может обрабатывать как данные, так и варианты планирования.

Пример

Следующая тестируемая система содержит простое состояние гонки между двумя потоками, обращающимися к одной и той же переменной. d деления на ноль, в операторах (1) и (2), что может привести к исключению если (1) выполняется до (2)

public class Racer implements Runnable {
     int d = 42;

     public void run() {
          doSomething(1001);
          d = 0;                              // (1)
     }

     public static void main(String[] args) {
          Racer racer = new Racer();
          Thread t = new Thread(racer);
          t.start();

          doSomething(1000);
          int c = 420 / racer.d;              // (2)
          System.out.println(c);
     }
     
     static void doSomething(int n) {
          try { Thread.sleep(n); } catch (InterruptedException ix) {}
     }
}

Без какой-либо дополнительной настройки JPF найдет и сообщит о делении на ноль. Если JPF настроен на проверку отсутствия условий гонки (независимо от их потенциальных последствий в дальнейшем), он выдаст следующий вывод, объясняющий ошибку и показывающий встречный пример, приводящий к ошибке.

JavaPathfinder v6.0 - (C) RIACS/NASA Ames Research Center
====================================================== system under test
application: Racer.java
...
====================================================== error #1
gov.nasa.jpf.listener.PreciseRaceDetector
race for field [email protected]
  main at Racer.main(Racer.java:16)
		"int c = 420 / racer.d;               "  : getfield
  Thread-0 at Racer.run(Racer.java:7)
		"d = 0;                               "  : putfield

====================================================== trace #1
---- transition #0 thread: 0
...
---- transition #3 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet[id="sleep",isCascaded:false,{main,>Thread-0}]
      [3 insn w/o sources]
  Racer.java:22                  : try { Thread.sleep(n); } catch (InterruptedException ix) {}
  Racer.java:23                  : }
  Racer.java:7                   : d = 0;                      
...
---- transition #5 thread: 0
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet[id="sharedField",isCascaded:false,{>main,Thread-0}]
  Racer.java:16                  : int c = 420 / racer.d;

Расширяемость

JPF — открытая система, которую можно расширять различными способами. Основные конструкции расширения:

слушатели — для реализации сложных свойств (например, временных свойств)
одноранговые классы — для выполнения кода на уровне JVM хоста (вместо JPF), который в основном используется для реализации собственных методов.
фабрики байт-кода — для обеспечения альтернативной семантики выполнения инструкций байт-кода (например, для реализации символьного выполнения)
генераторы выбора - для реализации ветвей пространства состояний, таких как выбор планирования или наборы значений данных.
сериализаторы — для реализации абстракций состояния программы.
издатели - для создания различных выходных форматов
политики поиска - использовать различные алгоритмы обхода пространства состояний программы.

JPF включает систему модулей времени выполнения для упаковки таких конструкций в отдельные проекты расширения JPF . На главном сервере JPF доступен ряд таких проектов, включая режим символического выполнения, числовой анализ, обнаружение состояния гонки для моделей с ослабленной памятью, проверку модели пользовательского интерфейса и многое другое.

Ограничения

JPF не может анализировать собственные методы Java . Если тестируемая система вызывает такие методы, они должны быть предоставлены в одноранговых классах или перехвачены слушателями.
в качестве средства проверки модели JPF подвержен комбинаторному взрыву , хотя он выполняет на лету частичное уменьшение порядка.
система конфигурации модулей JPF и параметров времени выполнения может быть сложной

См. также

MoonWalker — аналог Java PathFinder, но для программ .NET вместо программ Java.

Внешние ссылки

Ссылки

Виллем Виссер, Корина С. Пасэряну , Сарфраз Хуршид. Тестирование генерации входных данных с помощью Java PathFinder. В: Джордж С. Аврунин, Грегг Ротермель (ред.): Материалы Международного симпозиума ACM/SIGSOFT по тестированию и анализу программного обеспечения, 2004 г. ACM Press, 2004. ISBN 1-58113-820-2 .
Виллем Виссер, Клаус Хавелунд, Гийом Брат, Сынджун Пак, Флавио Лерда, Программы проверки моделей, Автоматизированная разработка программного обеспечения 10 (2), 2003.
Клаус Хавелунд, Виллем Виссер, Проверка модели программы как новая тенденция, STTT 4 (1), 2002.
Клаус Хавелунд, Томас Прессбургер, Проверка моделей программ Java с использованием Java PathFinder, STTT 2 (4), 2000.