[rules-dev] Formal verification of Drools - master's thesis

[Jiri Svitak]

Hello,

I work for Redhat as BRMS QE and I have to choose topic for my master's 
(diploma) thesis. It would be convenient for me to combine my job and 
the school thesis. I would like to know your opinions to following ideas:

1. Static analysis of Drools code with Findbugs. I have already talked 
with Geoffrey and he said that you use Findbugs, but only for common 
Findbugs scenarios. The thesis would then cover user defined bug 
patterns for common bugs based on bug reports or your experience.

2. Model checking of Drools with JavaPathFinder. Model checking verifies 
property of system by exploring state space of the system. The property 
is described by CTL or LTL logic (general example: given a concurrent 
program, we ask whether it is deadlock-free)

3. Different topic.

I would like to know your opinions and views if you would find that 
useful. If you have some tips on features to verify, on common bugs 
which could be found by these methods.  Also if you'll be willing to 
answer some questions about Drools source code if needed.

Thank you in advance.

Best regards

Jiri Svitak