Istituto di Scienza e Tecnologie dell'Informazione     
Ter Beek M. H., Massink M., Latella D., Gnesi S., Forghieri A., Sebastianis M. Model checking publish/subscribe notification for thinkteam. In: Electronic Notes in Theoretical Computer Science, vol. 133 pp. 275 - 294. J. Bicarregui; A. Butterfield; A. Arenas (ed.). Elsevier, 2005.
This paper reports on the fruitful combination of academic experience with formal modelling techniques and industrial experience with requirements exploration. We study the addition of a publish/subscribe notification service to thinkteama, a ready-to-use Product Data Management application developed by think3. thinkteam allows enterprises to capture, organise, automate, and share engineering product information and it is an example of an asynchronous and dispersed group-ware system. We define an abstract specification (model) of the groupware protocol underlying thinkteam and augment it with a publish/subscribe notification service. Consequently, we show a number of important correctness properties of the thinkteam model, some of which are also relevant to groupware protocols in general. In particular, we show that by adding a publish/subscribe notification service to thinkteam, the user's awareness of the status of the development of the engineering product and the activities of the design team increases.
URL: http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75H1-4G65CG5-J&_user=
Subject Publish/subscribe notification
Model checking
Concurrency control
D.2.4 Software/Program Verification. Model checking

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional