2006 | OriginalPaper | Buchkapitel
Towards Model Checking Stochastic Aspects of the thinkteam User Interface
verfasst von : Maurice H. ter Beek, Mieke Massink, Diego Latella
Erschienen in: Interactive Systems. Design, Specification, and Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Stochastic model checking is a recent extension of traditional model-checking techniques for the integrated analysis of both qualitative and
quantitative
system properties. In this paper we show how stochastic model checking can be conveniently used to address a number of usability concerns that involve quantitative aspects of a user interface for the industrial groupware system
thinkteam
.
thinkteam
is a ready-to-use Product Data Management application developed by
think3
. It allows enterprises to capture, organise, automate, and share engineering product information and it is an example of an asynchronous and dispersed groupware system. Several aspects of the functional correctness, such as concurrency aspects and awareness aspects, of the groupware protocol underlying
thinkteam
and of its planned publish/subscribe notification service have been addressed in previous work by means of a traditional model-checking approach. In this paper we investigate the trade-off between two different design options for granting users access to files in the database: a retrial approach and a waiting-list approach and show how stochastic model checking can be used for such analyses.