文章基本信息

标题：Assisting Groupware Development with Model Checking – Case Studies from Cooperative Work in the WWW
本地全文：下载
作者：Constantinos Papadopoulos
期刊名称：The Open Information Systems Journal
电子版ISSN：1874-1339
出版年度：2007
卷号：1
页码：1-18
DOI：10.2174/1874133900701010001
出版社：Bentham open
摘要：
Efficient collaboration entails significant benefits for modern enterprises. Recent advances in Internet technology allow physically dispersed groups to bypass the obstacles raised by geographical distances, so the development of Internet based groupware may extend collaboration to a global scale. As groupware applications grow larger and more diverse, however, it becomes difficult to anticipate their correctness. In this paper, we address this difficulty within the context of group awareness, which we regard both as a communication issue and a user-interface one. The main contribution of our research is the use of symbolic model checking for verifying group awareness in collaborative work across the WWW. This involves the specification of two related protocols with temporal logic and the development of a methodology for encoding temporal formulae into the language of a symbolic model checker, which eliminates the need to draw state-transition diagrams. Taking then advantage of the model checker's ability to produce counterexamples, we discover drawbacks in these protocols and propose thereon a number of improvements, which aim to transform the WWW into a reliable collaborative environment.