Formal Collaboration Protocols:

First-class Interaction Semantics for Multi-user Distributed Systems

David Stotts

Dept. of Computer Science
Univ. of North Carolina at Chapel Hill

NSF grant #IRI-9732577

Papers published

Collaborative software systems of the future will be far more complex than the simple systems we have today. As information transmission technology improves, we will be able to support multi-user applications that more nearly equal the complexity of interactions people naturally have face-to-face. This project will develop the formal structure necessary to reliably produce and maintain collaborative systems that are far more complex than today's systems.

This is a focussed investigation in formal methods for collaborative software systems, and is an outgrowth of earlier investigations in Trellis multi-user hypermedia and interoperable virtual environments.

We will first develop a specification method for defining intricate rules of collaborative interaction in a group computing application, and we will then produce analysis algorithms for verifying the correctness of the rules. We call such group rules {\em collaboration protocols}. To make these concepts available to system designers, we will also embody collaboration protocols in a set of distributed system services (as might be included in a developers library) and we will develop software engineering guidelines for employing these protocol services to best advantage in the software architecture of a collaborative system.

Collaboration protocols in current shared applications are implicitly defined by code segments scattered throughout the source for the application. A better method from a software engineering viewpoint is to explicitly define the collaboration semantics and implement it specifically as an identifiable module in the system. The advantages of this are:

  1. ease of reading and understanding the rules;
  2. formal notation allows analysis for errors;
  3. ease of developing collaborative systems with modular components;
  4. dynamic replacement of rules as collaboration progresses is possible.
We will illustrate the advantages of modular collaboration protocols by building and evaluating several complex systems: a group Web browsing (CobWeb) that allows many different interaction protocols; multi-user virtual environments (VEs); and an implementation of Nomic.

What are collaboration protocols?

We will investigate use of what we call collaboration protocols to define and manage the interactions of multiple users in a collaborative application. The technical issues to be examined include the specification notation(s) to use and the mechanisms for enacting and enforcing the rules across distributed networks. We list in this section some of the requirements for full specification of group interactions.

Collaboration protocols must capture in a formal notation these aspects of group interactions:

This list is just a starting point. We expect to discover more characteristics as work progresses.

In addition to capturing informational aspects of group interactions, a full specification must be in a formal notation so that analysis and reasoning algorithms may be developed and applied in support of system development and execution.

Collaboration protocols must be unambiguous and formal. Informal notation convey information to humans but do not support analysis and automated reasoning.

Collaboration protocols must however be flexible, not unusably rigid. People are not automata; this is what makes CSCW so fascinating as an area of study. They often need guidelines more than "rules". They need freedom to relax or sidestep rules when circumstances are not adequately covered by those rules. As people discover better methods and processes, the rules need to allow modifications and updates. We want to develop a protocol specification method that will be both formal and flexible. Rules need to be malleable while still conveying clear semantic information to the system using them. People need to feel in control of a system, not controlled by a system.

Specification methods

Colored P/T net for simple moderated meeting protocol

We will examine several technical methods for effectiveness in specifying collaboration protocols: colored Petri-nets (Trellis); tuple spaces (Linda); object-oriented database (similar to MOO, but in Java); knowledge base and inference engine (Ontolingua from Stanford). There may be other techniques that come to our attention during the investigation. We will include them in the study as we come to them.

As stated earlier, a collaboration protocol must be formal and flexible. We expect some combination of these techniques to be necessary to satisfy all the requirements we outlined. For example, a colored net will be very good for expressing possible parallel actions and synchronizations among members of a group. A knowledge base, however, would probably be better at allowing "bending" of the rules, with the inference engine helping to determine how much bending can be done before the process is compromised. A Java object might be best for capturing the basic data (who, what, when, where, etc.) characteristics of a protocol, but may be less analyzable for correctness than a net. We expect our studies to lead to a hybrid notation employing aspects of each of the following techniques.