An eclipse plug-in for the Java PathFinder runtime verification system

F. Arcelli; C. Raibulet; I. Rigo; L. Ubezio

doi:10.1109/SEW.2006.8

An eclipse plug-in for the Java PathFinder runtime verification system

F. Arcelli, C. Raibulet, I. Rigo, L. Ubezio

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

Abstract

Java PathFinder (JPF) is an explicit state model checker developed by the Automated Software Engineering Group of NASA of the AMES Research Center (California). Eclipse is probably the most important and used Java Integrated Developing Environment (IDE) and not only; it is a framework/environment that can be easily extended with new functionalities by exploiting its plug-in mechanism. Through a JPF plug-in for Eclipse it is possible to integrate powerful model checking and testing capabilities into the development environment. This paper presents the re-design of the standalone version of JPF towards an Eclipse plug-in exploiting and outlining in this way the advantages of an open source development. © 2006 IEEE.

Original language	English
Title of host publication	Proceedings of the 30th Annual IEEE/NASA Software Engineering Workshop, SEW-30
Pages	142-149
DOIs	https://doi.org/10.1109/SEW.2006.8
Publication status	Published - 2006
Externally published	Yes
Event	30th Annual IEEE/NASA Software Engineering Workshop, SEW-30 - , United States Duration: 24 Apr 2006 → 28 Apr 2006

Conference

Conference	30th Annual IEEE/NASA Software Engineering Workshop, SEW-30
Country/Territory	United States
Period	24/04/06 → 28/04/06

Access to Document

10.1109/SEW.2006.8

Persistent URL (handle)

Persistent link

Cite this

@inproceedings{eb226317d6734bfead417a7fb973fa5d,

title = "An eclipse plug-in for the Java PathFinder runtime verification system",

abstract = "Java PathFinder (JPF) is an explicit state model checker developed by the Automated Software Engineering Group of NASA of the AMES Research Center (California). Eclipse is probably the most important and used Java Integrated Developing Environment (IDE) and not only; it is a framework/environment that can be easily extended with new functionalities by exploiting its plug-in mechanism. Through a JPF plug-in for Eclipse it is possible to integrate powerful model checking and testing capabilities into the development environment. This paper presents the re-design of the standalone version of JPF towards an Eclipse plug-in exploiting and outlining in this way the advantages of an open source development. {\textcopyright} 2006 IEEE.",

author = "F. Arcelli and C. Raibulet and I. Rigo and L. Ubezio",

year = "2006",

doi = "10.1109/SEW.2006.8",

language = "English",

pages = "142--149",

booktitle = "Proceedings of the 30th Annual IEEE/NASA Software Engineering Workshop, SEW-30",

note = "30th Annual IEEE/NASA Software Engineering Workshop, SEW-30 ; Conference date: 24-04-2006 Through 28-04-2006",

}

TY - GEN

T1 - An eclipse plug-in for the Java PathFinder runtime verification system

AU - Arcelli, F.

AU - Raibulet, C.

AU - Rigo, I.

AU - Ubezio, L.

PY - 2006

Y1 - 2006

N2 - Java PathFinder (JPF) is an explicit state model checker developed by the Automated Software Engineering Group of NASA of the AMES Research Center (California). Eclipse is probably the most important and used Java Integrated Developing Environment (IDE) and not only; it is a framework/environment that can be easily extended with new functionalities by exploiting its plug-in mechanism. Through a JPF plug-in for Eclipse it is possible to integrate powerful model checking and testing capabilities into the development environment. This paper presents the re-design of the standalone version of JPF towards an Eclipse plug-in exploiting and outlining in this way the advantages of an open source development. © 2006 IEEE.

AB - Java PathFinder (JPF) is an explicit state model checker developed by the Automated Software Engineering Group of NASA of the AMES Research Center (California). Eclipse is probably the most important and used Java Integrated Developing Environment (IDE) and not only; it is a framework/environment that can be easily extended with new functionalities by exploiting its plug-in mechanism. Through a JPF plug-in for Eclipse it is possible to integrate powerful model checking and testing capabilities into the development environment. This paper presents the re-design of the standalone version of JPF towards an Eclipse plug-in exploiting and outlining in this way the advantages of an open source development. © 2006 IEEE.

UR - https://www.scopus.com/pages/publications/42949159537

UR - https://www.scopus.com/inward/citedby.url?scp=42949159537&partnerID=8YFLogxK

U2 - 10.1109/SEW.2006.8

DO - 10.1109/SEW.2006.8

M3 - Conference contribution

SP - 142

EP - 149

BT - Proceedings of the 30th Annual IEEE/NASA Software Engineering Workshop, SEW-30

T2 - 30th Annual IEEE/NASA Software Engineering Workshop, SEW-30

Y2 - 24 April 2006 through 28 April 2006

ER -

An eclipse plug-in for the Java PathFinder runtime verification system

Abstract

Conference

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this