| dbo:Software/fileSize
| |
| dbo:abstract
|
- Java Pathfinder (JPF) is a system to verify executable Java bytecode programs. JPF was developed at the NASA Ames Research Center and open sourced in 2005. The acronym JPF is not to be confused with the unrelated Java Plugin Framework project. The core of JPF is a Java Virtual Machine. JPF executes normal Java bytecode programs and can store, match and restore program states. Its primary application has been Model checking of concurrent programs, to find defects such as data races and deadlocks. With its respective extensions, JPF can also be used for a variety of other purposes, including
* model checking of distributed applications
* model checking of user interfaces
* test case generation by means of symbolic execution
* low level program inspection
* program instrumentation and runtime monitoring JPF has no fixed notion of state space branches and can handle both data and scheduling choices. (en)
- 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. (ru)
|
| dbo:developer
| |
| dbo:fileSize
|
- 1600000.000000 (xsd:double)
|
| dbo:genre
| |
| dbo:latestReleaseDate
| |
| dbo:latestReleaseVersion
| |
| dbo:license
| |
| dbo:operatingSystem
| |
| dbo:programmingLanguage
| |
| dbo:wikiPageExternalLink
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 6693 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| dbp:developer
| |
| dbp:genre
|
- Software verification tool, Virtual machine (en)
|
| dbp:latestReleaseDate
| |
| dbp:latestReleaseVersion
| |
| dbp:license
| |
| dbp:name
| |
| dbp:operatingSystem
| |
| dbp:programmingLanguage
| |
| dbp:size
| |
| dbp:website
| |
| dbp:wikiPageUsesTemplate
| |
| dbp:wordnet_type
| |
| dcterms:subject
| |
| gold:hypernym
| |
| rdf:type
| |
| rdfs:comment
|
- Java Pathfinder (JPF) is a system to verify executable Java bytecode programs. JPF was developed at the NASA Ames Research Center and open sourced in 2005. The acronym JPF is not to be confused with the unrelated Java Plugin Framework project. The core of JPF is a Java Virtual Machine. JPF executes normal Java bytecode programs and can store, match and restore program states. Its primary application has been Model checking of concurrent programs, to find defects such as data races and deadlocks. With its respective extensions, JPF can also be used for a variety of other purposes, including (en)
- Java PathFinder (JPF) — свободный инструмент для проверки многопоточных Java программ. По своей сути это виртуальная Java машина (англ. Java Virtual Machine) на основе которой реализованы методы проверки моделей (англ. model checking). Это означает, что JPF выполняет программу не один раз, как это делает обычная виртуальная машина, а по всем возможным путям, связанным с переключением потоков планировщиком. JPF находит такие ошибки как тупики, необработанные исключения, а также нарушения условий, задаваемых пользователем в виде assert выражений. Кроме того, пользователь может писать специальные слушатели (англ. listener-extensions) для проверки произвольных свойств. Некоторые из таких слушателей, такие как состояния гонок и ограничения на кучу (англ. heap bounds) поставляются вместе с JPF. (ru)
|
| rdfs:label
|
- Java Pathfinder (en)
- Java PathFinder (ru)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:homepage
| |
| foaf:isPrimaryTopicOf
| |
| foaf:name
| |
| is dbo:wikiPageDisambiguates
of | |
| is dbo:wikiPageWikiLink
of | |
| is foaf:primaryTopic
of | |
