Hello,
Is there a way to make JPF model check temporal logic assertions?
The original version of JPF supported LTL but then the support was dropped.
What is the reason for not supporting temporal logic?
How hard would it be to add such support?
I found the following paragraph in the mailing list:
From: Peter C. Mehlitz <pcmehlitz@em...> - 2005-07-12 16:33
...
One thing I had in mind for a while was using DynamicAssertions to do
temporal stuff(i.e. turn part of the property into an JPF object, and use
something like AspectJ to do the instrumentation), but there's no example
for this yet. The other way to do temporal logic by means of the LTL2Buchi
extension is not functional anymore - Dimitra's translator works fine, but
the LTLSearch is certainly defunct (until somebody fixes it, hint, hint).
Has anybody explored these tracks? has someone fixed LTLSearch?
Thanks,
David
|
