Re: [infinispan-dev] Formal verification (thesis)

Hi Jakub, interesting topic! Here are some areas where an investigation would be fruitful, in no particular order: Correctness of reads and writes in a distributed cache wrt state transfer: - Model gets and puts against a distributed data store - Run the model checker against this and see that there's no scenario where we can end up with inconsistent data - Add state transfer into the fold Split brain / network partitions: - Model a network partition, clients continue accessing the same values - Remove the split - Make sure the data in all nodes is consistent - Simulate multiple network partitions, e.g. from {A,B,C,D,E} -> {ABC} and {DE}, then {ABC} -> {AB} and {C} etc This may be too complex to model in TLA+, have you considered looking into Jepsen/Knossos as well? You'd have to talk to the Infinispan team to see what behavior is guaranteed by which configuration and then use these tools to make sure the actual behavior == the expected behavior. Cheers, On 13/01/16 16:56, Jakub Senko wrote: -- Bela Ban, JGroups lead (http://www.jgroups.org)