Jump to content


 


Register a free account to unlock additional features at BleepingComputer.com
Welcome to BleepingComputer, a free community where people like yourself come together to discuss and learn how to use their computers. Using the site is easy and fun. As a guest, you can browse and view the various discussions in the forums, but can not create a new topic or reply to an existing one unless you are logged in. Other benefits of registering an account are subscribing to topics and forums, creating a blog, and having no ads shown anywhere on the site.


Click here to Register a free account now! or read our Welcome Guide to learn how to use this site.

Photo

How Does Java Pathfinder's Model Checking Works


  • Please log in to reply
4 replies to this topic

#1 beanpole

beanpole

  • Members
  • 14 posts
  • OFFLINE
  •  
  • Local time:04:31 PM

Posted 18 May 2007 - 02:37 AM

Recently,my classmates and i do some research on jpf.We want to know how java pathfinder's model checking works and we need your help.I expect you give us some information.Useful websites and books are all ok,thanks for your help.

BC AdBot (Login to Remove)

 


#2 groovicus

groovicus

  • Security Colleague
  • 9,963 posts
  • OFFLINE
  •  
  • Gender:Male
  • Location:Centerville, SD
  • Local time:02:31 AM

Posted 18 May 2007 - 07:13 AM

The website tells you how it works. What more do you need?
http://javapathfinder.sourceforge.net/

it is a Java Virtual Machine (JVM) that is used as an explicit state software model checker, systematically exploring all potential execution paths of a program to find violations of properties like deadlocks or unhandled exceptions.

Maybe I don't understand your question?

#3 beanpole

beanpole
  • Topic Starter

  • Members
  • 14 posts
  • OFFLINE
  •  
  • Local time:04:31 PM

Posted 18 May 2007 - 09:19 AM

i just want to know how the model checker of jpf works,for example,how does jpf's model checker check deadlock out?
what is the principle ? the method to realize it?

Edited by beanpole, 18 May 2007 - 09:23 AM.


#4 groovicus

groovicus

  • Security Colleague
  • 9,963 posts
  • OFFLINE
  •  
  • Gender:Male
  • Location:Centerville, SD
  • Local time:02:31 AM

Posted 18 May 2007 - 10:21 AM

Therer are about 20 papers on the site that explain all of that. Deadlock is easy to test; if no more instructions are being executed, and the applciation is not waiting for input, and there is no normal termination flag, then the program is deadlocked. I have no clue exactly how it is executed in the program, but I suppose one could view the source code if one was interested enough.

#5 beanpole

beanpole
  • Topic Starter

  • Members
  • 14 posts
  • OFFLINE
  •  
  • Local time:04:31 PM

Posted 19 May 2007 - 05:46 AM

Thank you!I had known how jpf works,perhaps we need to view the source code to find out how it is executed in the programme.




0 user(s) are reading this topic

0 members, 0 guests, 0 anonymous users