PUMA
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. The document has been submitted to other: Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS'04), Technical report, 2004.
 
 
Abstract
(English)
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 thinkteam, 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 groupware 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.
Subject Publish/subscribe notification, thinkteam, model checking,asynchronous and dispersed groupware, awareness, concurrency control
D.2.4 Software/Program Verification..model checking : formal methods


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