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 Cæsar-Aldébarab toolbox.
Chapter PDF
Similar content being viewed by others
References
R. Allen and D. Garlan. Formal connectors. Technical report, Carnegie Mellon University, School of Computer Science, Pittsburgh, PA 15213, 1994.
R. Baiter, Slim Ben Atallah, and Rushed Kanawati. Architecture for syn chronous groupware application development. In HCI, Tokyo, Japan, july 1995.
T. Bolognesi and E. Brinksma. Introduction to the iso specification language lotos. 14 (1): 25–29, January 1988.
R. Baiter, L. Bellissard, S. Ben Attallah, F. Boyer, D. Demitrescu, R. Kanawati, A. Kerbrat, E. Lenormand, D. Lutoff, V. Marangozov, M. Riveill, and J.Y. Vion-Dury. Objectifs et orientations de l’action olan. Technical report, Bull-IMAG/Systèmes, 2 avenue de Vignates, 38610, Gières, 1995.
T. Crowley and al. Mmconf: An infrastructure for building shared multimedia applications. In CSCW;90, page 329, Los Angeles, October 1990.
N. Dulay. Darwin overview. Technical report, DSE Imperial College, London, 1994.
J.C. Fernandez, H. Garavel, L. Mounier, A. Rasse, C. Rodriguez, and J. Sifakis. A toolbox for the verification of lotos programs. In Lori A. Clarke, editor, Proceedings of the 14th International Conference on Software Engineering ICSE’14 (Melbourne, Australia), pages 246–259, New-York, May 1992. ACM.
Object Management Group. The common object request broker: Architecture and specification. Technical report, December 1993.
G.J. Holzmann. Algorithms for automated protocol validation. In Joseph Sifakis, editor, Proceedings of the 1st International Workshop on Automatic Verification Methods for Finite State Systems (Grenoble, France), June 1989.
S. Greenberg M. Roseman. Groupkit: A groupware toolkit for building real-time conferencing applications. In CSCW’92, page 43, November 1992.
Jean-Pierre Queille and Joseph Sifakis. Fairness and related properties in transition systems — a temporal logic to deal with fairness. Acta Informatica, 19: 195–220, 1983.
Mary Shaw. Procedure calls are the assembly language of software interconnection. Technical report, Carnegie Mellon University, School of Computer Science, Pittsburgh, PA 15213, 1994.
Daniel M. Yellin and Robert E. Strom. Interface, protocols and the semiautomatic contruction of software adaptors. Technical report, IBM T.J. Watson Research Center, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Kerbrat, A., Atallah, S.B. (1996). Formal Specification of a Framework for Groupware Development. In: Bochmann, G.v., Dssouli, R., Rafiq, O. (eds) Formal Description Techniques VIII. FORTE 1995. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34945-9_22
Download citation
DOI: https://doi.org/10.1007/978-0-387-34945-9_22
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2958-9
Online ISBN: 978-0-387-34945-9
eBook Packages: Springer Book Archive