An Eclipse Plug-in for the Java PathFinder Runtime Verification System

Author

Arcelli, Francesca ; Raibulet, Claudia ; Rigo, Ivano ; Ubezio, Luigi

Author_Institution

Dipt. di Informatica Sistemistica e Communicazione, Univ. degli Studi di Milano-Bicocca, Milan

fYear

2006

fDate

38808

Firstpage

142

Lastpage

152

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

Keywords

Java; formal verification; programming environments; public domain software; Java PathFinder runtime verification system; Java integrated developing environment; eclipse plug-in; open source development; state model checker; Automatic control; Engines; Graphics; Java; NASA; Software engineering; Software systems; Telecommunication control; Testing; User interfaces;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering Workshop, 2006. SEW '06. 30th Annual IEEE/NASA

Conference_Location

Columbia, MD

ISSN

1550-6215

Print_ISBN

0-7695-2624-1

Type

conf

DOI

10.1109/SEW.2006.8

Filename

4090255