Automated Verification of Groupware Protocols

by Maurice ter Beek, Mieke Massink, Diego Latella, Stefania Gnesi, Alessandro Forghieri and Maurizio Sebastianis

Recently, researchers from the Formal Methods and Tools (FM&&T) group of ISTI-CNR teamed up with researchers from think3, a global provider of integrated product development solutions. The goal was to apply formal modelling and verification techniques to enhance think3's Product Data Management (PDM) application, ‘thinkteam' (a registered trademark of think3 Inc) with a publish/subscribe notification service.

Computer-Supported Cooperative Work (CSCW) is an interdisciplinary research field which deals with understanding how people work together and finding ways in which computer technology can assist. This technology mostly consists of multi-user computer systems called groupware (systems). Many concepts and techniques from computer science, like concurrency control and data consistency, need to be rethought in the groupware domain. This has led to the development of new formal models like team automata, which were introduced explicitly for the description and analysis of groupware systems (see [TA] for details). Groupware systems are typically classified according to two dichotomies, namely (i) whether the users are working together at the same time (synchronous) or at different times (asynchronous) and (ii) whether they are working together in the same place (co-located) or in different places (dispersed). Examples of synchronous groupware include video conferencing and multi-user games, while electronic mail and the version-control systems which are often used in software engineering to coordinate changes made by multiple programmers to the same program are examples of asynchronous groupware.

An additional difficulty that arises during the design of synchronous groupware is the inherently distributed nature of such systems, which makes it necessary to address issues like network communication, concurrency control and distributed notification. This has led to the development of groupware toolkits that aid developers with programming abstractions aimed at simplifying the development of groupware applications.

We are currently modelling and verifying the addition of a publish/subscribe notification service to thinkteam, think3's PDM application catering to the product/document management needs for design processes in the manufacturing industry. The main strengths of this service are a rapid deployment and start-up cycle, flexibility, and a seamless integration with thinkdesign - think3's CAD solution - as well as with other third party products. Thinkteam allows enterprises to capture, organise, automate, and share engineering product information in an efficient way. The controlled storage and retrieval of document data in PDM applications is traditionally called vaulting, where the vault is a file-system-like repository. Its two main functions are (i) to provide a single, secure and controlled storage environment in which the documents controlled by the PDM application are managed, and (ii) to prevent inconsistent updates or changes to the document base while still allowing the maximal level of access compatible with the business rules. While the first function is integrated in the lower layers of the vaulting system, the second function is implemented in thinkteam's underlying groupware protocol by a standard set of operations on the vault, namely get (extract a read-only copy of a document), import (insert an external document), checkout (extract an exclusive copy of a document with the intent of modifying it), checkin (replace an edited and previously checked-out document), checkinout (replace an edited document in the vault, while at the same time retaining it as checked out), and uncheckout (cancel the effects of a checkout). Figure 1 shows a screen shot of thinkteam.

Figure 1: A thinkteam user checks out a document from the vault.

Thinkteam is thus an example of an asynchronous and dispersed groupware system. In order to develop the publish/subscribe notification service we first had to define an abstract specification (model) of the groupware protocol underlying thinkteam. The idea behind this type of service is to more widely inform the users of an application by intelligent data sharing. For instance, whenever a user publishes a file by sending it to a centralised repository, all users who subscribe to that file are notified automatically via a multicast communication. The automatic verification of publish/subscribe notification services is currently attracting a lot of attention. The addition of such a service to thinkteam should allow us to solve a problem that commonly arises in connection with the use of composite documents and which is a variant of the classic 'lost update' phenomenon, depicted in Figure 2. This phenomenon arises when a user performs a checkout/modify/checkin cycle on a document that may be used as reference copy by other users.

Figure 2: The 'lost update' phenomenon.

Our research shows that with relatively simple models we can verify highly relevant properties of groupware protocols with freely available verification tools. Model checking is an automatic technique to verify whether a system design satisfies its specifications. The verification is exhaustive, ie all possible input combinations and states are taken into account. One of the best-known and most successful model checkers is Spin, which was developed at Bell Labs during the last two decades. It offers a spectrum of verification techniques, is freely available, and is very well documented. Publish/ subscribe systems require specific properties, including data consistency through distributed notification, view consistency, absence of (user) starvation and key issues related to concurrency control [BMLG]. The properties we verify are mostly formalised as formulae of a Linear Temporal Logic (LTL). This has the advantage that they are close to the 'scenarios' design. LTL formulae reflect properties of typical behaviour (or uses) of the groupware system. This makes it possible to evaluate design alternatives before their implementation and validation and not only afterwards. Design errors constitute up to 40% of software errors and are among the most expensive to resolve when discovered only after the implementation phase. Our system allows these to be detected early on in development, leading to considerable reductions in cost and improvements in quality. The specification (model) of thinkteam's underlying groupware protocols has been developed using this methodology and in close collaboration between members of FM&&T and think3.

This research is conducted within the framework of a broader national research project on global computing, funded by the Italian Ministry of Research and Education (MIUR/SP4).

Links:
[TA]: http://fmt.isti.cnr.it/~mtbeek/TA.html
[BMLG]: http://fmt.isti.cnr.it/WEBPAPER/TR-61.pdf
FM&&T: http://fmt.isti.cnr.it/
think3: http://www.think3.com/
Spin: http://www.spinroot.com/

Please contact:
Maurice ter Beek, Mieke Massink
ISTI-CNR, Italy
E-mail: {terbeek,massink}@isti.cnr.it