Java Pathfinder (JPF) - это система для проверки исполняемых программ с байт-кодом Java . JPF был разработан в Исследовательском центре NASA Ames Research Center, и его исходный код был открыт в 2005 году. Аббревиатуру JPF не следует путать с несвязанным проектом Java Plugin Framework .
Разработчики) | НАСА |
---|---|
Стабильный выпуск | 6.0 / 30 ноября 2010 г. |
Написано в | Ява |
Операционная система | Кроссплатформенность |
Размер | 1,6 МБ (в архиве) |
Тип | Инструмент проверки программного обеспечения , Виртуальная машина |
Лицензия | Версия лицензии Apache 2 |
Веб-сайт | https://github.com/javapathfinder/ |
Ядром JPF является виртуальная машина Java . JPF выполняет обычные программы с байт-кодом Java и может сохранять, сопоставлять и восстанавливать состояния программ. Его основным применением была проверка моделей параллельных программ для поиска дефектов, таких как скачки данных и взаимоблокировки . С соответствующими расширениями JPF также может использоваться для множества других целей, в том числе
- проверка моделей распределенных приложений
- модельная проверка пользовательских интерфейсов
- генерация тестового случая посредством символьного выполнения
- проверка программы низкого уровня
- программный инструментарий и мониторинг времени выполнения
JPF не имеет фиксированного понятия ветвей пространства состояний и может обрабатывать как данные, так и варианты планирования.
Пример
Следующая тестируемая система содержит простое условие гонки между двумя потоками, обращающимися к одной и той же переменной d
в операторах (1) и (2), что может привести к исключению деления на ноль, если (1) выполняется до (2).
открытый класс Racer реализует Runnable { int d = 42 ; public void run () { doSomething ( 1001 ); d = 0 ; // (1) } public static void main ( String [] args ) { Racer racer = new Racer (); Тема t = новая тема ( гонщик ); т . start (); doSomething ( 1000 ); int c = 420 / гонщик . d ; // (2) Система . из . println ( c ); } static void doSomething ( int n ) { попробуйте { Thread . сон ( н ); } catch ( InterruptedException ix ) {} } }
Без какой-либо дополнительной настройки JPF найдет и сообщит о делении на ноль. Если JPF настроен для проверки отсутствия условий гонки (независимо от их потенциальных последствий в нисходящем направлении), он выдаст следующий вывод, объясняющий ошибку и показывающий пример счетчика, ведущего к ошибке.
JavaPathfinder v6.0 - (C) RIACS / NASA Исследовательский центр Эймса================================================== ==== тестируемая системаприложение: Racer.java...================================================== ==== ошибка №1gov.nasa.jpf.listener.PreciseRaceDetectorгонка за поле [email protected] main в Racer.main (Racer.java:16)"int c = 420 / racer.d;": getfield Тема-0 на Racer.run (Racer.java:7)"d = 0;": putfield================================================== ==== след №1---- переход # 0 поток: 0...---- переход № 3 поток: 1gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet [id = "sleep", isCascaded: false, {main,> Thread-0}] [3 insn без источников] Racer.java:22: попробуйте {Thread.sleep (n); } catch (InterruptedException ix) {} Racer.java:23:} Racer.java:7: d = 0; ...---- переход № 5 поток: 0gov.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.