Formal Specification of a Framework for Groupware Development

Alain Kerbrat and Slim Ben Atallah

Proceedings of the 8th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols {FORTE}'95 (Montreal, Quebec, Canada), October 1995

Abstract:

This paper describes the formal specification in Lotos of CoopScan, a framework for cooperative applications development. We first present the architectural choices and collaboration strategies for the integration of applications in such a collaboration aware framework. Then, we show how we derive a Lotos specification from the CoopScan description. We define some generic properties to be verified in this kind of framework. The verification of some of these properties is presented, using the Caesar-Aldebaran toolbox.

8 pages

PDF

PostScript