Sorry for not responding earlier, it's proposal season and everybody is=20=
a bit busy.
There are two ways to implement properties, both described in the docu=20=
under "how to implement properties": gov.nasa.jpf.Property and=20
VM/SearchListener.
As a rule of thumb, I would say the older 'Property' is more for simple=20=
conditions where you just have to query some existing (more complex)=20
state of the VM or the Search to find out if the property holds (like=20
NoUncaughtExceptionsProperty, NotDeadlockedProperty etc.). The=20
Listeners are more versatile, but naturally you have to do more. There=20=
is a mistake in the docu, which says that you can use=20
Search.terminate() to indicate failure, but I somehow went with the=20
scheme of implementing the Property interface in the Listener, then=20
just query the internal Listener state in the Property.check() (no=20
changes to Search classes required that way). Look at=20
gov.nasa.jpf.tools.HeapTracker as an example. If you are in doubt=20
because your property looks complicated, I would say this is almost=20
certainly the right way to go - there are no limits what you can do=20
here.
Safety property, that is. One thing I had in mind for a while was using=20=
DynamicAssertions to do temporal stuff (i.e. turn part of the property=20=
into an JPF object, and use something like AspectJ to do the=20
instrumentation), but there's no example for this yet. The other way to=20=
do temporal logic by means of the LTL2Buchi extension is not functional=20=
anymore - Dimitra's translator works fine, but the LTLSearch is=20
certainly defunct (until somebody fixes it, hint, hint).
hope this helps a bit
-- Peter
On Jul 7, 2005, at 6:55 PM, M=EDrian Bruckschen wrote:
> Hi all,
>
> We're an undergraduate group of students and we're trying to verify
> some properties in a work a friend of us has done, that is an
> object-oriented DMBS.
>
> We have simplified the most we could the code, and we started by
> verifying the DBMS server. Or tried to.
>
> We've read the documentation available at the site, and have chosen to
> verify using listeners (cause we need to step by the states generated,
> and it seemed to us the best way to do it). But we are not really
> confident of how to specify the properties. Is there any simpler
> documentation on it? Can anybody point us the right way to go? How can
> we specify properties for JPF to verify using listeners?
>
> Thanks for your attention,
|
