Towards Model Checking Stochastic Aspects of the thinkteam User Interface

  • Maurice H. ter Beek
  • Mieke Massink
  • Diego Latella
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3941)


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.


Model Check Retrial Rate Temporal Logic Retrial Queue Request Rate 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Henzinger, T.: Reactive modules. Formal Methods in System Design 15, 7–48 (1999)CrossRefGoogle Scholar
  2. 2.
    Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model checking continuous time Markov chains. ACM Transactions on Computational Logic 1(1), 162–170 (2000)CrossRefMathSciNetGoogle Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    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),
  6. 6.
    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)Google Scholar
  7. 7.
    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),
  8. 8.
    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)Google Scholar
  9. 9.
    Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.): Lectures on Formal Methods and Performance Analysis. LNCS, vol. 2090. Springer, Heidelberg (2001)zbMATHGoogle Scholar
  10. 10.
    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)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Cairns, P., Jones, M., Thimbleby, H.: Reusable usability analysis with Markov models. ACM Transactions on Computer Human Interaction 8(2), 99–132 (2001)CrossRefGoogle Scholar
  12. 12.
    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)zbMATHCrossRefGoogle Scholar
  13. 13.
    Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  14. 14.
    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)Google Scholar
  15. 15.
    Dourish, P., Bellotti, V.: Awareness and coordination in shared workspaces. In: Proc. CSCW 1992, pp. 107–114. ACM Press, New York (1992)CrossRefGoogle Scholar
  16. 16.
    Ellis, C.A., Gibbs, S.J., Rein, G.L.: Groupware—Some issues and experiences. Communications of the ACM 34(1), 38–58 (1991)CrossRefGoogle Scholar
  17. 17.
    Falin, G.I.: A survey of retrial queues. Queueing Systems 7, 127–168 (1990)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Falin, G.I., Templeton, J.G.C.: Retrial Queues. Chapman and Hall, Boca Raton (1997)zbMATHGoogle Scholar
  19. 19.
    Haverkort, B.: Markovianmodels for performance and dependability evaluation. In: [9], pp. 38–83Google Scholar
  20. 20.
    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)CrossRefGoogle Scholar
  21. 21.
    Hillston, J.: A Compositional Approach to Performance Modelling. CU Press, Cambridge (1996)Google Scholar
  22. 22.
    Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley, Reading (2003)Google Scholar
  23. 23.
    Kulkarni, V.: Modeling and Analysis of Stochastic Systems. Chapman and Hall, Boca Raton (1995)zbMATHGoogle Scholar
  24. 24.
    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)CrossRefGoogle Scholar
  25. 25.
    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)CrossRefGoogle Scholar
  26. 26.
    Papadopoulos, C.: An extended temporal logic for CSCW. Comp. Journal 45, 453–472 (2002)zbMATHCrossRefGoogle Scholar
  27. 27.
    Urnes, T.: Efficiently Implementing Synchronous Groupware. Ph.D. thesis, Department of Computer Science, York University, Toronto (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Maurice H. ter Beek
    • 1
  • Mieke Massink
    • 1
  • Diego Latella
    • 1
  1. 1.CNR/ISTI – ‘A. Faedo’PisaItaly

Personalised recommendations