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 |
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:
Collaboration protocols must capture in a formal notation these aspects of group interactions:
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.
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.