Abstract
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.
This work has been partially funded by the EU project AGILE (IST-2001-32747). For further details, the reader is referred to the technical report of this paper [5].
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alur, R., Henzinger, T.: Reactive modules. Formal Methods in System Design 15, 7–48 (1999)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model checking continuous time Markov chains. ACM Transactions on Computational Logic 1(1), 162–170 (2000)
Baier, C., Katoen, J.-P., Hermanns, H.: Approximate symbolic model checking of continuoustime Markov chains. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 146–162. Springer, Heidelberg (1999)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Automated performance and dependability evaluation using model checking. In: Calzarossa, M.C., Tucci, S. (eds.) Performance 2002. LNCS, vol. 2459, pp. 261–289. Springer, Heidelberg (2002)
ter Beek, M.H., Massink, M., Latella, D.: Towards Model Checking Stochastic Aspects of the thinkteam User Interface—FULL VERSION. Technical Report 2005-TR-18, CNR/ISTI (2005), http://fmt.isti.cnr.it/WEBPAPER/TRdsvis.pdf
ter Beek, M.H., Massink, M., Latella, D., Gnesi, S.: Model checking groupware protocols. In: Cooperative Systems Design, pp. 179–194. IOS Press, Amsterdam (2004)
ter Beek, M.H., Massink, M., Latella, D., Gnesi, S., Forghieri, A., Sebastianis, M.: Model checking publish/subscribe notification for thinkteam, Technical Report 2004-TR-20, CNR/ISTI (2004), http://fmt.isti.cnr.it/WEBPAPER/TRTT.ps
ter Beek, M.H., Massink, M., Latella, D., Gnesi, S., Forghieri, A., Sebastianis, M.: Model checking publish/subscribe notification for thinkteam. In: Proc. FMICS 2004. ENTCS, vol. 133, pp. 275–294 (2005)
Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.): Lectures on Formal Methods and Performance Analysis. LNCS, vol. 2090. Springer, Heidelberg (2001)
Buchholz, P., Katoen, J.-P., Kemper, P., Tepper, C.: Model-checking large structured Markov chains. Journal of Logic and Algebraic Programming 56, 69–96 (2003)
Cairns, P., Jones, M., Thimbleby, H.: Reusable usability analysis with Markov models. ACM Transactions on Computer Human Interaction 8(2), 99–132 (2001)
Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8, 244–263 (1986)
Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Doherty, G., Massink, M., Faconti, G.P.: Reasoning about interactive systems with stochastic models. In: Johnson, C. (ed.) DSV-IS 2001. LNCS, vol. 2220, pp. 144–163. Springer, Heidelberg (2001)
Dourish, P., Bellotti, V.: Awareness and coordination in shared workspaces. In: Proc. CSCW 1992, pp. 107–114. ACM Press, New York (1992)
Ellis, C.A., Gibbs, S.J., Rein, G.L.: Groupware—Some issues and experiences. Communications of the ACM 34(1), 38–58 (1991)
Falin, G.I.: A survey of retrial queues. Queueing Systems 7, 127–168 (1990)
Falin, G.I., Templeton, J.G.C.: Retrial Queues. Chapman and Hall, Boca Raton (1997)
Haverkort, B.: Markovianmodels for performance and dependability evaluation. In: [9], pp. 38–83
Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: A tool for model-checking Markov chains. Int. Journal on Software Tools for Technology Transfer 4, 153–172 (2003)
Hillston, J.: A Compositional Approach to Performance Modelling. CU Press, Cambridge (1996)
Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley, Reading (2003)
Kulkarni, V.: Modeling and Analysis of Stochastic Systems. Chapman and Hall, Boca Raton (1995)
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 52–66. Springer, Heidelberg (2002)
Lacaze, X., Palanque, P., Navarre, D., Bastide, R.: Performance Evaluation as a Tool for Quantitative Assessment of Complexity of Interactive Systems. In: Forbrig, P., Limbourg, Q., Urban, B., Vanderdonckt, J. (eds.) DSV-IS 2002. LNCS, vol. 2545, pp. 208–222. Springer, Heidelberg (2002)
Papadopoulos, C.: An extended temporal logic for CSCW. Comp. Journal 45, 453–472 (2002)
Urnes, T.: Efficiently Implementing Synchronous Groupware. Ph.D. thesis, Department of Computer Science, York University, Toronto (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
ter Beek, M.H., Massink, M., Latella, D. (2006). Towards Model Checking Stochastic Aspects of the thinkteam User Interface. In: Gilroy, S.W., Harrison, M.D. (eds) Interactive Systems. Design, Specification, and Verification. DSV-IS 2005. Lecture Notes in Computer Science, vol 3941. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11752707_4
Download citation
DOI: https://doi.org/10.1007/11752707_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-34145-1
Online ISBN: 978-3-540-34146-8
eBook Packages: Computer ScienceComputer Science (R0)