Hello Jakub, not only are we interested: we have been talking about it for a while, but lack of time has not allowed us to pursue it. So yes, it would be very useful. As far as scope it seems like you already have a good grasp of what to tackle, and we are more than happy to answer any questions you might have. I would like both Bela Ban and Richard Achmatowicz to add their thoughts to this, as they have more intimate knowledge with the tools and the concepts behind formal verification.
Tristan On 13/01/2016 16:56, Jakub Senko wrote: > Hi all! > > I'm considering a thesis topic [1] inspired by the successful use > of automated formal verification methods by Amazon engineers for AWS S3 and > others [2]. > > The basic idea is to use similar tools to verify core parts of Infinispan > by constructing a simplified model (because of the state space explosion). > Most useful areas seem to be the transport layer, command object execution > (get, put, topology change, state transfer), entry locks etc. > On the other hand, I'd exclude transactional operations > which would be too complicated/costly to verify. > > Do you think this would be useful for you as the infinispan developers? > Do you have suggestions on what (not) to focus? > I'd be happy for any comments. > > Cheers, > Jakub Senko > > [1] > https://diplomky.redhat.com/topic/show/355/formal-design-of-distributed-hash-table > [2] > http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext > _______________________________________________ > infinispan-dev mailing list > [email protected] > https://lists.jboss.org/mailman/listinfo/infinispan-dev > -- Tristan Tarrant Infinispan Lead JBoss, a division of Red Hat _______________________________________________ infinispan-dev mailing list [email protected] https://lists.jboss.org/mailman/listinfo/infinispan-dev
