A case study on the automated verification of groupware protocols

We report on a fruitful combination of applying academic experience with formal modelling and verification techniques to an industrial case study. The goal of the case study was to investigate a priori, i.e. before implementation, the effects of adding a lightweight and easy-to-use publish/subscribe (event) notification service to thinkteam® - an asynchronous and dispersed groupware system which was developed by think3. Researchers from the Formal Methods and Tools (FM&&T) group of ISTI-CNR $with a longstanding experience in research on the development and application of formal methods, notations, and software tools for the specification, design, and verification of complex computer systems - therefore teamed up with think3 - a global provider of integrated product development solutions that provides mechanical design and Product Data Management (PDM) software catering the product management needs of design processes in the manufacturing industry. The technical details of this joint research effort have been documented elsewhere, here we report on the lessons learned from this experience.