beanpole
May 18 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.
groovicus
May 18 2007, 07:13 AM
The website tells you how it works. What more do you need?
http://javapathfinder.sourceforge.net/QUOTE
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?
beanpole
May 18 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?
groovicus
May 18 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.
beanpole
May 19 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.
This is a "lo-fi" version of our main content. To view the full version with more information, formatting and images, please
click here.