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

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