No Access

AN AUTOMATA-BASED APPROACH TO CSCW VERIFICATION

CONSTANTINOS PAPADOPOULOS

Department of Computing, University of Manchester Institute of Science and Technology, P. O. Box 88, Manchester M60 1 QD, UK

Search for more papers by this author

https://doi.org/10.1142/S0218843004000936Cited by:1 (Source: Crossref)

Abstract

Software development for computer-supported cooperative work (CSCW) is a notoriously difficult task, involving often concurrent processes which are bound up with rigid timing constraints. To cope effectively with this difficulty, we propose in this paper the use of abstract finite-state models. The utility of these models is illustrated by encoding a CSCW system that we have built into finite-state automata, specifying in them a number of desired properties with temporal logic, and verifying these properties with model checking. By incorporating timing constraints into this process, we also gain insight into the usability of our system in real cooperative scenarios.

Keywords:

References

R. Alur and D. Dill, Theoretical Computer Science 126(2), 183 (1994), DOI: 10.1016/0304-3975(94)90010-8. Crossref, Web of Science, Google Scholar
N. S. Barghouti and G. E. Kaiser, ACM Computing Surveys 23(3), 269 (1991), DOI: 10.1145/116873.116875. Crossref, Web of Science, Google Scholar
J. M. Begole, Flexible collaboration transparency: Supporting worker independence in replicated application sharing-systems, PhD thesis, Department of Computer Science, Virginia Technology, Virginia (1998) . Google Scholar
S. Bødkeret al., Computer support for cooperative design, Proc. 2nd ACM CSCW Conf (ACM Press, New York, 1988) pp. 377–394. Google Scholar
A. Boualiet al., The FC2TOOLS set, Proc. 8th Int. Conf. Computer-Aided Verification1102, Lecture Notes in Computer Science (Springer-Verlag, Berlin, Germany) pp. 441–445. Google Scholar
J. Campbell, Concurrency control for real-time diagramming, PhD thesis, Department of Information Science and Telecommunications, University of Pittsburgh, Pennsylvania (2001) . Google Scholar
E. M. Clarke , O. Grumberg and D. A. Peled , Model Checking ( MIT Press , Cambridge, MA , 1999 ) . Google Scholar
E. M. Clarke, E. A. Emerson and A. P. Sistla, ACM Trans. Programming Languages and Systems 8(2), 244 (1986), DOI: 10.1145/5397.5399. Crossref, Web of Science, Google Scholar
E. M. Clarke and R. Kurshan, IEEE Spectrum 33(6), 61 (1996), DOI: 10.1109/6.499951. Crossref, Web of Science, Google Scholar
A. Dix, Pace and interaction, People and Computers VII, Proc. HCI '92 Conf. (Cambridge University Press, Cambridge, UK, 1992) pp. 193–207. Google Scholar
P. Dourish and V. Bellotti, Awareness and coordination in shared workspaces, Proc. 4th ACM CSCW Conf. (ACM Press, New York) pp. 107–114. Google Scholar
C. Ellis and S. Gibbs, Concurrency control in groupware systems, Proc. 10th ACM SIGMOD Conf. (ACM Press, New York) pp. 399–407. Google Scholar
E. A. Emerson and J. Srinivasan, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Lecture Notes in Computer Science 354 (Springer, Heidelberg, Germany) pp. 123–172. Crossref, Google Scholar
N. Francez , Fairness ( Springer-Verlag , Heidelberg, Germany , 1986 ) . Crossref, Google Scholar
P. Godefroidet al., Ensuring privacy in pres ence awareness systems: An automated verification approach, Proc. 8th ACM CSCW Conf. (ACM Press, New York) pp. 59–68. Google Scholar
S. Greenberg and M. Roseman, GroupKit: A groupware toolkit for building real-time conferencing applications, Proc. 4th ACM CSCW Conf. (ACM Press, New York) pp. 43–50. Google Scholar
C. Gutwin and S. Greenberg, The mechanics of collaboration: Developing low-cost usability evaluation methods for shared workspaces, Proc. 9th WET ICE Workshop (IEEE Computer Society Press, Los Alamitos, CA) pp. 98–103. Google Scholar
M. Harrison and J. Torres (eds.) , Proc. Design, Specification and Verification of Interactive Systems '97 Workshop ( Springer-Verlag , Heidelberg, Germany ) . Google Scholar
J. Hopcroft , R. Motwani and J. Ullman , Introduction to Automata Theory, Languages and Computation , 2nd edn. ( Addison-Wesley , New York , 2000 ) . Google Scholar
Y. J. Joung, Distributed Computing 13(4), 189 (2000), DOI: 10.1007/PL00008918. Crossref, Web of Science, Google Scholar
K. G. Larsen, P. Pettersen and W. Yi, Compositional and symbolic model checking for real-time systems, Proc. 16th Real-Time Systems Symp. (IEEE Computer Society Press, Los Alamitos, CA) pp. 76–87. Google Scholar
S. Lu and J. Cai, Annals of the CIRP 49(1), 69 (2000), DOI: 10.1016/S0007-8506(07)62898-4. Crossref, Google Scholar
Z. Manna and A. Pnueli , Temporal Verification of Reactive Systems-Safety ( Springer , Heidelberg, Germany , 1995 ) . Crossref, Google Scholar
Z. Manna, S. Ness and J. Vuillemin, Inductive methods for proving properties of programs, Proc. ACM Conf. Proving Assertions about Programs (ACM Press, New York) pp. 27–50. Google Scholar
R. Milner , Communication and Concurrency ( Prentice-Hall , Englewood Cliffs, NJ , 1990 ) . Google Scholar
J. Munson and P. Dewan, A concurrency control framework for collaborative systems, Proc. 6th ACM CSCW Conf. (ACM Press, New York) pp. 278–287. Google Scholar
C. Papadopoulos, Int. Journal Cooperative Information Systems 11(1/2), 21 (2002), DOI: 10.1142/S0218843002000492. Link, Web of Science, Google Scholar
C. Papadopoulos, The Computer Journal 45(4), 453 (2002), DOI: 10.1093/comjnl/45.4.453. Crossref, Web of Science, Google Scholar
C. Papadopoulos, A concurrency control framework for cooperative design, PhD thesis, Computing Department, Lancaster University, UK (2003) . Google Scholar
C. S. Pasareanu, M. B. Dwyer and M. Huth, Assume-guarantee model checking of software: A comparative case study, Proc. 6th Int SPIN Workshop on the Theoretical and Practical Aspects of the SPIN Model Checker (Springer-Verlag, London, UK) pp. 168–183. Google Scholar
A. Prakashet al., Corona: A communication service for scaleable, reliable group collaboration systems, Proc. 6th ACM CSCW Conf. (ACM Press, New York) pp. 140–149. Google Scholar
M. Ressel, D. Nitsche-Ruhland and R. Gunzenhäuser, An integrated transformation-oriented approach to concurrency control and undo in group editors, Proc. 6th ACM CSCW Conf. (ACM Press, New York) pp. 288–297. Google Scholar
K. Schmidt, P. Carstensen and U. Wiil, Supporting shop floor intelligence: A CSCW approach to production planning and control in flexible manufacturing, Proc. 2nd ACM Group Conf. (ACM Press, New York) pp. 111–120. Google Scholar
G. Smith and J. O'Brien, Re-coupling tailored user interfaces, Proc. 7th ACM CSCW Conf. (ACM Press, New York) pp. 237–246. Google Scholar
M. P. Steveset al., A comparison of usage evaluation and inspection methods for assessing group ware usability, Proc. 3rd ACM GROUP Conf. (ACM Press, New York) pp. 125–134. Google Scholar
P. D. Stotts and R. Furutta, Interpreted collaboration protocols and their use in groupware prototyping, Proc. 5th ACM CSCW Conf. (ACM Press, New York) pp. 121–130. Google Scholar
C. Sun and D. Chen, Undoing any operation in collaborative graphics editing systems, Proc. 3rd ACM Group Conf. (ACM Press, New York) pp. 197–206. Google Scholar
C. Sun and D. Chen, ACM Trans. Computer-Human Interaction 9(1), 1 (2002), DOI: 10.1145/505151.505152. Crossref, Web of Science, Google Scholar
C. Sunet al., ACM Trans. Computer-Human Interaction 5(1), 63 (1998), DOI: 10.1145/274444.274447. Crossref, Google Scholar
J. Tsai and E. Juan , Compositional Verification of High-Assurance Systems ( Kluwer , Boston, MA , 1999 ) . Google Scholar
www.docs.uu.se/docs/rtmv/uppaal . Google Scholar
J. F. K. A. Van Benthem , The Logic of Time: A Model-Theoretic Investigation into the Varieties of Temporal Ontology and Temporal Discourse ( Kluwer , Reidel, MA , 1982 ) . Google Scholar
www.bell-labs.com/projects/verisoft . Google Scholar
http://www.go.dlr.de/cgi-bin/man?xforms . Google Scholar
J. Yang, A. K. Mok and F. Wang, ACM Trans. Programming Languages and Systems 19(2), 386 (1997), DOI: 10.1145/244795.244803. Crossref, Web of Science, Google Scholar