Patrice Godefroid
James D. Herbsleb
ABSTRACT
Providing information about other users and their activites is a central function of many collaborative applications. The data that provide this "presence awareness" are usually automatically generated and highly dynamic. For example, services such as AOL Instant Messenger allow users to observe the status of one another and to initiate and participate in chat sessions. As such services become more powerful, privacy and security issues regarding access to sensitive user data become critical. Two key software engineering challenges arise in this context:
Policies regarding access to data in collaborative applications have subtle complexities, and must be easily modifiable during a collaboration.
Users must be able to have a high degree of confidence that the implementations of these policies are correct.
In this paper, we propose a framework that uses an automated verification approach to ensure that such systems conform to complex policies. Our approach takes advantage of VeriSoft, a recent tool for systematically testing implementations of concurrent systems, and is applicable to a wide variety of specification and development platforms for collaborative applications. we illustrate the key features of our framework by applying it to the development of a presence awareness system.
- 1.G. D. Abowd. Software engineering issues for ubiquitous computing. In International Conference on Software Engineering, 1999. Google Scholar
Digital Library
- 2.B. Alpern and F. B. Schneider. Recognizing safety and liveness. Distributed Computing, 2:117-126, 1987.Google ScholarDigital Library
- 3.V. Bellotti, A. Blandford, D. Duke, A. MacLean, J. May, and L. Nigay. Interpersonal access control in computermediated communications: A systematic analysis of the design space. Human-Computer Interaction, 11:357- 432, 1996. Google ScholarDigital Library
- 4.A. Bullock and S. Benford. An access control framework for multi-user collaborative environments. In Proceedings GROUP '99, pages 140-149, Phoenix, AZ, November 1999. Google ScholarDigital Library
- 5.R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: A semantics based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems, 1(15):36-72, 1993. Google ScholarDigital Library
- 6.C. Colby, L. J. Jagadeesan, R. Jagadeesan, K. L~aufer, and C. Puchol. Objects and concurrency in Triveni: A telecommunication case study in Java. In 4th USENIX Conference on Object Oriented Technologies and Systems, April 1998. Google ScholarDigital Library
- 7.W. K. Edwards. Policies and roles in collaborative applications. In Proc. of ACM Conf. on CSCW, 1996. Google ScholarDigital Library
- 8.J. Fernandez, H. Garavel, L. Mounier, A. Rasse, C. Rodriguez, and J. Sifakis. A toolbox for the verification of LOTOS programs. In International Conference on Software Engineering, May 1992. Google ScholarDigital Library
- 9.L. Fuchs. Area: A cross-application notification service for groupware. In Proceedings of the Sixth European Conference on Computer-supported Cooperative Work, pages 61-80, Copenhagen, Denmark, September 1999. Google ScholarDigital Library
- 10.B. Gaver, T. Moran, A. MacLean, L. Levstrand, P. Dourish, K. Carter, , and B. Buxton. Realizing a video environment: Europarc's rave system. In Conference on Human Factors in Computing Systems, 1992. Google ScholarDigital Library
- 11.P. Godefroid. Model Checking for Programming Languages using VeriSoft. In ACM Symposium on Principles of Programming Languages, pages 174-186, January 1997. Google ScholarDigital Library
- 12.P. Godefroid, R. S. Hanmer, and L. J. Jagadeesan. Model Checking Without a Model: An Analysis of the Heart- Beat Monitor of a Telephone Switch using VeriSoft. In ACM SIGSOFT International Symposium on Software Testing and Analysis, March 1998. Google ScholarDigital Library
- 13.J. Grudin. Why cscw applications fail: Problems in the design and evaluation of organizational interfaces. In Conference on Computer-Supported Cooperative Work CSCW '88, 1988. Google ScholarDigital Library
- 14.J. D. Herbsleb and R. E. Grinter. Architectures, coordination, and distance: Conway's law and beyond. IEEE Software, pages 63-70, Sept/Oct 1999. Google ScholarDigital Library
- 15.D. Hindus, M. S. Ackerman, S. Mainwaring, and B. Starr. Thunderwire: A field study of an audioonly media space. In Computer Supported Cooperative Work, 1996. Google ScholarDigital Library
- 16.G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991. Google ScholarDigital Library
- 17.S. E. Hudson and I. Smith. Techniques for addressing fundamental privacy and disruption tradeoffs in awareness support systems. In Computer Supported Cooperative Work, 1996. Google ScholarDigital Library
- 18.D. Li and R. R. Muntz. Coca: Collaborative objects coordination architecture. In Proceedings of ACM CSCW, Nov. 1998. Google ScholarDigital Library
- 19.D. Li and R. R. Muntz. A collaboration specification language. In Proceedings of the 2nd USENIX Conference on Domain Specific Languages, Oct 1999. Google ScholarDigital Library
- 20.Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer- Verlag, 1992. Google ScholarDigital Library
- 21.M. Mantei, R. Baecker, A. Sellen, W. Buxton, T. Milligan, , and B. Wellman. Experience in the use of a media space. In Proceedings of the CHI'91 Conference on Human Factors in Computing Systems, pages 203-208, 1991. Google ScholarDigital Library
- 22.S. E. McDaniel, G. M. Olson, and J. C. Magee. Identifying and analyzing multiple threads in computermediated and face-to-face conversations. In Computer Supported Cooperative Work, 1996. Google ScholarDigital Library
- 23.T. Nomura, K. Hayashi, T. Hazama, and S. Gudmundson. Interlocus: Workspace configuration mechanisms for activity awareness. In Computer Supported Cooperative Work, 1998. Google ScholarDigital Library
- 24.L. Palen. Social, individual, and technological issues for groupware calendar systems. In CHI'99, 1999. Google ScholarDigital Library
- 25.W. Prinz. Nessie: An awareness environment for cooperative settings. In European Conference on Computer Supported Cooperative Work, 1999. Google ScholarDigital Library
- 26.R. S. Sandhu, E. J. Coyne, H. L. Feinstein, , and C. E. Youman. Role-based access control models. IEEE Computer, 29(2):38-47, Feb. 1996. Google ScholarDigital Library
- 27.H. Shen and P. Dewan. Access control for collaborative systems. In Proc. of ACM Conf. on CSCW, 1992. Google ScholarDigital Library
- 28.M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In First Symposium on Logic in Computer Science, pages 322-331, June 1986.Google Scholar
- 29.R. Want, A. Hopper, V. Falcao, and J. Gibbons. The active badge location system. ACM Transactions on Information Systems, 10(1):91-102, 1992. Google ScholarDigital Library
- 30.E. Zaret. Upstart in the instant messager war. MSNBC, 1999.Google Scholar
- 31.Q. A. Zhao and J. T. Stasko. Evaluating image filtering based techniques in media space applications. In Proceedings of ACM CSCW, Nov 1998. Google ScholarDigital Library
Index Terms
- Ensuring privacy in presence awareness: an automated verification approach
Recommendations
Coordination challenges in a computer-supported meeting environment
Special issue: Organizational impact of group support systems, expert systems, and executive information systemsIn this study we observed the coordination activities of groups collaboratively writing in a low-structure computer-supported meeting room. We used video analyses of the sessions to identify well-coordinated and poorly coordinated groups. Through user ...
Formal Verification of Differential Privacy for Interactive Systems (Extended Abstract)
Differential privacy is a promising approach to privacy preserving data analysis with a well-developed theory for functions. Despite recent work on implementing systems that aim to provide differential privacy, the problem of formally verifying that ...
Measuring Awareness in Cross-Team Collaborations -- Distance Matters
ICGSE '13: Proceedings of the 2013 IEEE 8th International Conference on Global Software EngineeringDeveloping and maintaining team awareness within and across teams working in the same project helps team members in aligning their activities and facilitates implicit coordination. This requires both task and presence awareness. In this paper, we share ...
Comments