Skip to main content
SpringerLink
Log in

Model Checking of Control-User Component-Based Parametrised Systems

  • Conference paper
Component-Based Software Engineering (CBSE 2008)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5282))

Included in the following conference series:

Abstract

Many real component-based systems, so called Control-User systems, are composed of a stable part (control component) and a number of dynamic components of the same type (user components). Models of these systems are parametrised by the number of user components and thus potentially infinite. Model checking techniques can be used to verify only specific instances of the systems. This paper presents an algorithmic technique for verification of safety interaction properties of Control-User systems. The core of our verification method is a computation of a cutoff. If the system is proved to be correct for every number of user components lower than the cutoff then it is correct for any number of users. We present an on-the-fly model checking algorithm which integrates computation of a cutoff with the verification itself. Symmetry reduction can be applied during the verification to tackle the state explosion of the model. Applying the algorithm we verify models of several previously published component-based systems.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. http://fractal.objectweb.org/tutorial/index.html

  2. http://anna.fi.muni.cz/coin/CUmodels/

  3. Poetzsch-Heffter, A., Aldrich, J., Barnett, M., Giannakopoulou, D., Leavens, G.T., Sharygina, N.: Challenge Problem SAVCBS 2007 (May 2007), http://www.eecs.ucf.edu/leavens/SAVCBS/2007/challenge.shtml

  4. Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: LICS 1996. IEEE Computer Society, Los Alamitos (1996)

    Google Scholar 

  5. Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102. Springer, Heidelberg (2001)

    Google Scholar 

  6. Basu, S., Ramakrishnan, C.R.: Compositional analysis for verification of parameterized systems. Theor. Comput. Sci. 354(2), 211–229 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  7. Bulej, L., Bures, T., Coupaye, T., Decky, M., Jezek, P., Parizek, P., Plasil, F., Poch, T., Rivierre, N., Sery, O., Tuma, P.: CoCoME in Fractal. In: PACS 2000. LNCS, vol. 5153. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  8. Calder, M., Miller, A.: An automatic abstraction technique for verifying featured, parameterised systems. Theoretical Computer Science (to appear, 2008)

    Google Scholar 

  9. Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State/event-based software model checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  10. Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design 9(1-2), 77–104 (1996)

    Article  Google Scholar 

  11. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, USA (2000)

    Google Scholar 

  12. Clarke, E.M., Talupur, M., Veith, H.: Proving ptolemy right: The environment abstraction principle for model checking concurrent systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 33–47. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  13. Dickson, L.E.: Finiteness of the odd prerfect and primitive abundant numbers with r distinct prime factors. Amer. Journal Math. 35, 413–422 (1913)

    Article  MathSciNet  MATH  Google Scholar 

  14. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: FMSP, pp. 7–15. ACM Press, New York (1998)

    Chapter  Google Scholar 

  15. Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 236–254. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  16. Emerson, E.A., Kahlon, V.: Exact and efficient verification of parameterized cache coherence protocols. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 247–262. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  17. Emerson, E.A., Kahlon, V.: Model checking guarded protocols. In: LICS 2003, pp. 361–370. IEEE Computer Society, Los Alamitos (2003)

    Google Scholar 

  18. Emerson, E.A., Kahlon, V.: Rapid parameterized model checking of snoopy cache coherence protocols. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 144–159. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  19. Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: POPL 1995, pp. 85–94. ACM, New York (1995)

    Google Scholar 

  20. Fontaine, P., Gribomont, E.P.: Decidability of invariant validation for paramaterized systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 97–112. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  21. German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  22. Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 220–234. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  23. Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. Theor. Comput. Sci. 256, 93–112 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  24. Kofroň, J.: Behavior Protocols Extensions. PhD thesis, Charles University in Prague (2007)

    Google Scholar 

  25. Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. CWI Quarterly 2(3), 219–246 (1989)

    MathSciNet  MATH  Google Scholar 

  26. Maidl, M.: A unifying model checking approach for safety properties of parameterized systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 311–323. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  27. Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82–97. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  28. Pnueli, A., Zuck, L.D.: Model-checking and abstraction to the aid of parameterized systems. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, p. 4. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  29. Component reliability extensions for fractal component model, http://kraken.cs.cas.cz/ft/public/public_index.phtml

  30. Rybina, T., Voronkov, A.: Using canonical representations of solutions to speed up infinite-state model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  31. Vařeková, P., Černá, I.: Model Checking of Control-User Component-Based Parametrised Systems. Technical Report FIMU-RS-2008-06, Masaryk University, Faculty of Informatics, Brno, Czech Republic (2008)

    Google Scholar 

  32. Vařeková, P., Moravec, P., Černá, I., Zimmerova, B.: Effective-Verification of Systems with a Dynamic-Number of Components. In: SAVCBS 2007, pp. 3–13. ACM Press, New York (2007)

    Google Scholar 

  33. Vařeková, P., Zimmerova, B.: Solution of challenge problem. In: SAVCBS 2007. ACM Press, New York (2007)

    Google Scholar 

  34. Zimmerova, B., Vařeková, P.: Reflecting creation and destruction of instances in CBSs modelling and verification. In: MEMICS 2007, Znojmo, Czech Republic (2007)

    Google Scholar 

  35. Zimmerova, B., Vařeková, P., Beneš, N., Černá, I., Brim, L., Sochor, J.: Component-Interaction Automata Approach (CoIn). In: PACS 2000. LNCS, vol. 5153, pp. 146–176. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Informatics, Masaryk University, Czech Republic

    Pavlína Vařeková & Ivana Černá

Authors
  1. Pavlína Vařeková
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ivana Černá
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Technische Universiteit Eindhoven, Den Dolech 2, 5600MB, Eindhoven, The Netherlands

    Michel R. V. Chaudron

  2. Microsoft, USA

    Clemens Szyperski

  3. Chair for Software Design and Quality, University of Karlsruhe (TH),, Am Fasanengarten 5, 76131, Karlsruhe, Germany

    Ralf Reussner

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Vařeková, P., Černá, I. (2008). Model Checking of Control-User Component-Based Parametrised Systems. In: Chaudron, M.R.V., Szyperski, C., Reussner, R. (eds) Component-Based Software Engineering. CBSE 2008. Lecture Notes in Computer Science, vol 5282. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87891-9_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-87891-9_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-87890-2

  • Online ISBN: 978-3-540-87891-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation