Java PathFinder

Java PathFinder (JPF) — свободный инструмент для проверки многопоточных Java программ. По своей сути это виртуальная Java машина (англ. Java Virtual Machine) на основе которой реализованы методы проверки моделей (англ. model checking). Это означает, что JPF выполняет программу не один раз, как это делает обычная виртуальная машина, а по всем возможным путям, связанным с переключением потоков планировщиком. JPF находит такие ошибки как тупики, необработанные исключения, а также нарушения условий, задаваемых пользователем в виде assert выражений. Кроме того, пользователь может писать специальные слушатели (англ. listener-extensions) для проверки произвольных свойств. Некоторые из таких слушателей, такие как состояния гонок и ограничения на кучу (англ. heap bounds) поставляются вместе с JPF. При нахождении ошибки JPF выводит полную трассу, которая к ней ведет, включая все необходимые переключения планировщика.

В общем случае JPF способен проверять любые Java программы, которые не зависят от не поддерживаемых native методов. Виртуальная машина JPF не может выполнять платформенно зависимый код. Это накладывает существенные ограничения на то, какие стандартные библиотеки могут использоваться тестируемым приложением. Хотя в принципе возможно написать для этих библиотек специальные обертки (используя Model Java Interface), но на данный момент в JPF нет поддержки java.awt, java.net, и только ограниченная поддержка java.io и reflection. Другое ограничение JPF — по месту необходимому для хранения состояния, что ограничивает размеры проверяемых приложений до ~10kloc (в зависимости от их внутренней структуры). Для решения проблем масштабирования JPF предоставляет гибкие механизмы расширения, которые позволяют подстраивать его под конкретные приложения и проверяемые свойства. Кроме того, данные механизмы позволяют рассматривать JPF как framework для различного рода техник верификации. Из за ограничений на библиотеки и размер приложений JPF до настоящего времени использовался для приложений, которые являются моделями, но написаны на полноценном языке программирования Java.

JPF разработан в NASA. Распространяется под свободной лицензией NASA Open Source Agreement version 1.3.

• Model Checking Programs. W. Visser, K. Havelund, G. Brat, S. Park and F. Lerda. Automated Software Engineering Journal.Volume 10, Number 2, April 2003. [1]
• Addressing Dynamic Issues of Program Model Checking. F. Lerda and W. Visser. Proccedings of SPIN2001. Toronto, May 2001. [2]

• Официальный сайт