A case study on the automated verification of groupware protocols

ABSTRACT

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.

REFERENCES

• 1: Ronald M. Baecker, Readings in GroupWare and Computer-Supported Cooperative Work: Assisting Human-Human Collaboration, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1994
• 2: Maurice H. Ter Beek , Clarence A. Ellis , Jetty Kleijn , Grzegorz Rozenberg, Synchronizations in Team Automata for Groupware Systems, Computer Supported Cooperative Work, v.12 n.1, p.21-69, February 2003 [doi>10.1023/A:1022407907596]
• 3: M. H. ter Beek, M. Massink, D. Latella, and S. Gnesi. Model Checking Groupware Protocols. In F. Darses, R. Dieng, C. Simone, and M. Zacklad, editors, Cooperative Systems Design-Scenario-Based Design of Collaborative Systems, volume 107 of Frontiers in Artificial Intelligence and Applications, pages 179--194. IOS Press, Amsterdam, 2004.
• 4: M. H. ter Beek, M. Massink, D. Latella, S. Gnesi, A. Forghieri, and M. Sebastianis. Model Checking Publish/Subscribe Notification for thinkteam. Technical Report 2004-TR-20, Istituto di Scienza e Tecnologie dell'Informazione, Consiglio Nazionale delle Ricerche, 2004.
• 5: M. H. ter Beek, M. Massink, D. Latella, S. Gnesi, A. Forghieri, and M. Sebastianis. Automated Verification of Groupware Protocols. ERCIM News--Special: Automated Software Engineering, 58:33--35, July 2004.
• 6: M. Caporuscio, P. Inverardi, and P. Pelliccione. Formal Analysis of Clients Mobility in the Siena Publish/Subscribe Middleware. Technical report, Department of Computer Science, University of L'Aquila, 2002.
• 7: X. Deng, M. B. Dwyer, J. Hatcliff, G. Jung, Robby, and G. Singh. Model-Checking Middleware-Based Event-Driven Real-Time Embedded Software. In F. S. de Boer, M. M. Bonsangue, S. Graf, and W.-P. de Roever, editors, Proceedings FMCO'02, volume 2852 of LNCS, pages 154--181. Springer-Verlag, Berlin, 2002.
• 8: Paul Dourish , Victoria Bellotti, Awareness and coordination in shared workspaces, Proceedings of the 1992 ACM conference on Computer-supported cooperative work, p.107-114, November 01-04, 1992, Toronto, Ontario, Canada [doi>10.1145/143457.143468]
• 9: Clarence Ellis, Team automata for groupware systems, Proceedings of the international ACM SIGGROUP conference on Supporting group work: the integration challenge, p.415-424, November 16-19, 1997, Phoenix, Arizona, United States [doi>10.1145/266838.267363]
• 10: Clarence A. Ellis , Simon J. Gibbs , Gail Rein, Groupware: some issues and experiences, Communications of the ACM, v.34 n.1, p.39-58, Jan. 1991 [doi>10.1145/99977.99987]
• 11: Patrick Th. Eugster , Pascal A. Felber , Rachid Guerraoui , Anne-Marie Kermarrec, The many faces of publish/subscribe, ACM Computing Surveys (CSUR), v.35 n.2, p.114-131, June 2003 [doi>10.1145/857076.857078]
• 12: D. Garlan, S. Khersonsky, and J. S. Kim. Model Checking Publish-Subscribe Systems. In T. Ball and S. K. Rajamani, editors, Proceedings SPIN'03, volume 2648 of LNCS, pages 166--180. Springer-Verlag, Berlin, 2003.
• 13: Jonathan Grudin, Computer-Supported Cooperative Work: History and Focus, Computer, v.27 n.5, p.19-26, May 1994 [doi>10.1109/2.291294]
• 14: Carl Gutwin , Saul Greenberg , Mark Roseman, Supporting awareness of others in groupware, Conference companion on Human factors in computing systems: common ground, p.205, April 13-18, 1996, Vancouver, British Columbia, Canada [doi>10.1145/257089.257282]
• 15: G. J. Holzmann. The SPIN Model Checker--Primer and Reference Manual. Addison Wesley, Reading, MA, 2003.
• 16: J. Kleijn. Team Automata for CSCW - A Survey -. In H. Ehrig, W. Reisig, G. Rozenberg, and H. Weber, editors, Petri Net Technology for Communication-Based Systems--Advances in Petri Nets, volume 2472 of LNCS, pages 295--320. Springer-Verlag, Berlin, 2003.
• 17: P. Liggesmeyer, M. Rothfelder, M. Rettelbach, and T. Ackermann. Qualitatssicherung Software-basierter Technischer Systeme--Problembereiche und Lösungs-ansätze. Informatik Spektrum, 21(5):249--258, 1998.
• 18: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 19: C. Papadopoulos. An Extended Temporal Logic for CSCW. The Computer Journal, 45(4):453--472, 2002.
• 20: Kjeld Schmidt, The Problem with 'Awareness': Introductory Remarks on 'Awareness in CSCW', Computer Supported Cooperative Work, v.11 n.3, p.285-298, 2002 [doi>10.1023/A:1021272909573]
• 21: S. Tripakis and S. Yovine. Timing Analysis and Code Generation of Vehicle Control Software using Taxys. In K. Havelund and G. Rosu, editors, Proceedings RV'01, volume 55(2) of ENTCS, pages 174--183. Elsevier, Amsterdam, 2001.
• 22: Tore Urnes , T. C. Graham, Efficiently implementing synchronous groupware, 1999
• 23: L. Zanolin, C. Ghezzi, and L. Baresi. An Approach to Model and Validate Publish/Subscribe Architectures. In M. Barnett, S. H. Edwards, D. Giannakopoulou, and G. T. Leavens, editors, Proceedings SAVCBS'03, Technical Report 03-11, pages 35--41. Department of Computer Science, Iowa State University, 2003.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

General Terms:
Experimentation, Verification

Keywords:
groupware, model checking, publish/subscribe notification, thinkteam