Интернет магазин китайских планшетных компьютеров



Компьютеры - Java PathFinder

11 мая 2011





Java PathFinder — свободный инструмент для проверки многопоточных Java программ. По своей сути это виртуальная Java машина на основе которой реализованы методы проверки моделей. Это означает, что JPF выполняет программу не один раз, как это делает обычная виртуальная машина, а по всем возможным путям, связанным с переключением потоков планировщиком. JPF находит такие ошибки как тупики, необработанные исключения, а также нарушения условий, задаваемых пользователем в виде assert выражений. Кроме того, пользователь может писать специальные слушатели для проверки произвольных свойств. Некоторые из таких слушателей, такие как состояния гонок и ограничения на кучу поставляются вместе с JPF. При нахождении ошибки JPF выводит полную трассу, которая к ней ведет, включая все необходимые переключения планировщика.

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

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



Просмотров: 522


<<< OpenUP