Advertisement

Formal Design of Cooperative Systems

  • Michel Diaz
  • Thierry Villemur
  • François Vernadat
Chapter
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)

Abstract

This paper starts with a formal definition of the concept of cooperation in distributed systems. The proposed model is based on the use of graphs and of logic, where logic expresses contradiction and pragmatism. The dynamic structuring of such systems leads to the concept of multi-connection at the cooperation level and to a layered top-down formal design methodology. The protocol providing the multi-connection management or membership service will be specified and verified using the VAL tool and a Petri net based specification. It will be shown how the resulting system can be proven correct. The VAL description is then translated into an Estelle description that has been implemented on top of a distributed platform. Private possible conversation subgroups (PCSs) inside a cooperative group of agents have also been introduced.

Keywords

Cooperative work cooperative groups protocol design multi-agent system VAL Estelle formal specifications 

Bibliogra phy

  1. [AALS94]
    M. P. van de Aalst, K. M. van Hee and G. J. Houben. Modelling Workflow Management with High Level Petri Nets. Workshop on Computer Supported Cooperative Work, Petri Nets and related formalisms, Zaragoza, pages 31–50, June 1994.Google Scholar
  2. [AGOS94]
    A. Agostini, G. de Michelis and K. Petruni. Keeping Workflow Models as Simple as Possible. Workshop on Computer Supported Cooperative Work, Petri Nets and related formalisms, Zaragoza, pages 11–29, June 1994.Google Scholar
  3. [BANN89]
    L. J. Bannon et K. Schmidt: Four Characters in Search of a Context. In Studies in Computer Supported Cooperative Work: Theory, Practice and Design, Eds. J. M. Bowers and S. D. Benford, Elsevier, 1991.Google Scholar
  4. [BENF93]
    S. Benford and J. Palme. A Standard for OSI Group Communication. Computer Networks and ISDN systems, 25 (1993): 933–946. 1993.CrossRefGoogle Scholar
  5. [BLAI94]
    G. S. Blair and T. Rodden. The Opportunities and Challenges of CSCW. Journal of the Brazilian Computer Society, 1 (1): 3–14, July 1994.Google Scholar
  6. [BUDK87]
    S. Budkowski and P. Dembinski. An Introduction to Estelle: A specification Language for Distributed Systems. Computer Networks and ISDN Systems, 14 (1): 3–23, 1987.CrossRefGoogle Scholar
  7. [DIAZ82]
    M. Diaz. Modeling and Analysis of Communication and Cooperation Protocols Using Petri Net Based Models. Computer Networks 6 (6): 419–442, December 1982.zbMATHGoogle Scholar
  8. [DIAZ89]
    M. Diaz and C. Vissers. SEDOS: Designing Open Distributed Systems. IEEE Software 6 (6): 24–33, Novembre 1989.Google Scholar
  9. [DIAZ92]
    M. Diaz. A logical model of cooperation. Proceedings of the IEEE Third Workshop on Future Trends of Distributed Computing Systems, pages 64–70. April 1992.CrossRefGoogle Scholar
  10. [DIAZ93a]
    M. Diaz. Coopération, Logique et Partage de Données. Proceedings of the AFCET and AFIA. Premières Journées Francophones Intelligence Artificielle Distribuée et Systèmes Multi-Agents, pages 253–262. April 1993.Google Scholar
  11. [DIAZ93b]
    M. Diaz and T. Villemur. Membership Services and Protocols for Cooperative Frameworks of Processes. Computer Communications, 16 (9): 548–556. September 1993.CrossRefGoogle Scholar
  12. [DIAZ94]
    M. Diaz and T. Villemur. Formation of Private Conversation Subgroups in a Cooperative Group of Processes. Journal of the Brazilian Computer Society, 1 (I): 46–58, July 1994.Google Scholar
  13. [EC92]
    EC ESTELLE to C compiler. Version 3.0. User reference manual. BULL S.A Copyright 1989, 1990. INT Copyright 1991, 1992., EDB ESTELLE simulator debugger. Version 3.0. User reference manual. BULL S.A Copyright 1989, 1990. INT Copyright 1991, 1992.Google Scholar
  14. [EIJK88]
    P. Van Eijk, Ch. Vissers, M. Diaz Editors, The Formal Description Technique LOTOS, 1988, North- HollandGoogle Scholar
  15. [ELLI91]
    C. Ellis, S. Gibbs and G. Rein. Groupware. Some issues and experiences. Communications of the ACM, 34 (1): 38–58. January 1991.CrossRefGoogle Scholar
  16. [EMER89]
    E. A. Emerson, J. Srivanasan, Branching Time Temporal Logic, Lecture Notes in Computer Science, Volume 354, 1989.Google Scholar
  17. [FAGI85]
    R. Fagin, J. Y. Halpem. Belief, Awareness, and Limited Reasoning: Preliminary Report. 9th IJCAI 1985, Los Angeles, USA.Google Scholar
  18. [FERN88]
    J.C. Fernandez. Aldébaran, Un système de vérification par réduction de processus communicants. PhD thesis, Université de Grenoble, France, 1988.Google Scholar
  19. [HALP86]
    J. Y. Halpern. Reasoning about Knowledge: an Overview. Proceedings of the Conference of Theoretical Aspects of Reasoning about Knowledge, Ed. J. Y. Halpern, 1986.Google Scholar
  20. [HEWI91]
    C. Hewitt and J. Inman. DAI Betwixt and Between: From “Intelligent Agents” to Open System Science. IEEE Transactions on Systems, Man, and Cybernetics, 21 (6): 1409–1419. November/December 1991.Google Scholar
  21. [HUGH68]
    G. E. Hughes, M. J. Cresswell. An Introduction to Modal Logic. Methuen, 1968.Google Scholar
  22. [ISO9074]
    Information processing systems. Open System Interconnection. Estelle: A formal description technique based on an extended state transition model, ISO IS 9074, Juin 1989.Google Scholar
  23. [JUAN88]
    G. Juanole, O. Amyay, P. Azema, R. Gustaysson, B. Pershon. Towards a Knowledge-Base for Design of (N) Service-Protocol Pairs -An Epistemic Approach. In Research into Networks and Distributed Applications, Ed. R. Speth, North Holland, 1988.Google Scholar
  24. [KARS94]
    A. Karsenty. Le collecticiel: de l’ interaction homme-machine à la communication homme- machine-homme. Technique et science informatiques, 13 (1): 105–127, 1994.Google Scholar
  25. [KRAE88]
    K. L. Kraemer and J. L. King. Computer-Based Systems for Cooperative Work and Group Decision Making. ACM Computing Surveys, 20 (2): 115–146. June 1988.CrossRefGoogle Scholar
  26. [KRAS91]
    H. Krasner, J. Mclnroy and D. B. Walz. Groupware Research and Technology Issues with Application to Software Process Management. IEEE Transactions on Systems, Man, and Cybernetics, 21 (4): 704–712, July/August 1991.CrossRefGoogle Scholar
  27. [MANN89]
    Z. Manna, A. Pnueli. The Anchored Version of the Temporal Framework, Lecture Notes in Computer Science, Volume 354, 1989.Google Scholar
  28. [MILN80]
    R. Milner. CCS, a calculus for communicating systems, Lecture Notes in Computer Science 92, Springer Verlag 1980.Google Scholar
  29. [SHOH89]
    Y. Shoham, Y. Moses. Belief as Defeasible Knowledge. 11th IJCAI 1989, Detroit, USA.Google Scholar
  30. [VERN93]
    F. Vernadat and P. Azéma. Prototypage d’agents communicants. Proceedings of the AFCET and AFIA. Premières Journées Francophones Intelligence Artificielle Distribuée et Systèmes Multi-Agents, pages 129–140. April 1993.Google Scholar
  31. [VICT89]
    F. Victor and E. Sommer. Supporting the design of Office Procedures in the DOMINO System. In Studies in Computer Supported Cooperative Work: Theory, Practice and Design, Eds. J. M. Bowers and S. D. Benford, Elsevier, 1991.Google Scholar
  32. [VILL94]
    T. Villemur, M. Diaz, F. Vernadat and P. Azéma. Verification of Services and Protocols for Dynamic Membership to Cooperative Groups. Workshop on Computer Supported Cooperative Work, Petri Nets and related formalisms, Zaragoza, pages 73–91, June 1994.Google Scholar
  33. [WERN88]
    E. Werner. Towards a Theory of Communication and Cooperation for Multiagent Planning. Proceedings of the 2nd Conference of Theoretical Aspects of Reasoning About Knowledge, Ed. M. Y. Vardi, pages 129–144, 1988.Google Scholar
  34. [ZIMM80]
    H. ZIMMERMAN, OSI reference model, the ISO model of architecture for open systems interconnection, IEEE Trans. on Communications, vol. COM-28, April 1980.Google Scholar

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • Michel Diaz
    • 1
  • Thierry Villemur
    • 1
  • François Vernadat
    • 1
  1. 1.LAAS du CNRS 7TOULOUSE CedexFrance

Personalised recommendations