{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:49:37Z","timestamp":1725518977168},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540878902"},{"type":"electronic","value":"9783540878919"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-87891-9_10","type":"book-chapter","created":{"date-parts":[[2008,10,9]],"date-time":"2008-10-09T06:48:06Z","timestamp":1223534886000},"page":"146-162","source":"Crossref","is-referenced-by-count":1,"title":["Model Checking of Control-User Component-Based Parametrised Systems"],"prefix":"10.1007","author":[{"given":"Pavl\u00edna","family":"Va\u0159ekov\u00e1","sequence":"first","affiliation":[]},{"given":"Ivana","family":"\u010cern\u00e1","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"http:\/\/fractal.objectweb.org\/tutorial\/index.html"},{"key":"10_CR2","unstructured":"http:\/\/anna.fi.muni.cz\/coin\/CUmodels\/"},{"key":"10_CR3","unstructured":"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"},{"key":"10_CR4","volume-title":"LICS 1996","author":"P.A. Abdulla","year":"1996","unstructured":"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)"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"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.\u00a02102. Springer, Heidelberg (2001)"},{"issue":"2","key":"10_CR6","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/j.tcs.2005.11.016","volume":"354","author":"S. Basu","year":"2006","unstructured":"Basu, S., Ramakrishnan, C.R.: Compositional analysis for verification of parameterized systems. Theor. Comput. Sci.\u00a0354(2), 211\u2013229 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85289-6_14","volume-title":"The Common Component Modeling Example: Comparing Software Component Models","author":"L. Bulej","year":"2008","unstructured":"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.\u00a05153. Springer, Heidelberg (2008)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Calder, M., Miller, A.: An automatic abstraction technique for verifying featured, parameterised systems. Theoretical Computer Science (to appear, 2008)","DOI":"10.1016\/j.tcs.2008.03.034"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24756-2_8","volume-title":"Integrated Formal Methods","author":"S. Chaki","year":"2004","unstructured":"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.\u00a02999. Springer, Heidelberg (2004)"},{"issue":"1-2","key":"10_CR10","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"E.M. Clarke","year":"1996","unstructured":"Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design\u00a09(1-2), 77\u2013104 (1996)","journal-title":"Formal Methods in System Design"},{"key":"10_CR11","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, USA (2000)"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-78800-3_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.M. Clarke","year":"2008","unstructured":"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.\u00a04963, pp. 33\u201347. Springer, Heidelberg (2008)"},{"key":"10_CR13","doi-asserted-by":"publisher","first-page":"413","DOI":"10.2307\/2370405","volume":"35","author":"L.E. Dickson","year":"1913","unstructured":"Dickson, L.E.: Finiteness of the odd prerfect and primitive abundant numbers with r distinct prime factors. Amer. Journal Math.\u00a035, 413\u2013422 (1913)","journal-title":"Amer. Journal Math."},{"key":"10_CR14","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/298595.298598","volume-title":"FMSP","author":"M.B. Dwyer","year":"1998","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: FMSP, pp. 7\u201315. ACM Press, New York (1998)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/10721959_19","volume-title":"Automated Deduction - CADE-17","author":"E.A. Emerson","year":"2000","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 236\u2013254. Springer, Heidelberg (2000)"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-540-39724-3_22","volume-title":"Correct Hardware Design and Verification Methods","author":"E.A. Emerson","year":"2003","unstructured":"Emerson, E.A., Kahlon, V.: Exact and efficient verification of parameterized cache coherence protocols. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 247\u2013262. Springer, Heidelberg (2003)"},{"key":"10_CR17","first-page":"361","volume-title":"LICS 2003","author":"E.A. Emerson","year":"2003","unstructured":"Emerson, E.A., Kahlon, V.: Model checking guarded protocols. In: LICS 2003, pp. 361\u2013370. IEEE Computer Society, Los Alamitos (2003)"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/3-540-36577-X_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.A. Emerson","year":"2003","unstructured":"Emerson, E.A., Kahlon, V.: Rapid parameterized model checking of snoopy cache coherence protocols. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 144\u2013159. Springer, Heidelberg (2003)"},{"key":"10_CR19","first-page":"85","volume-title":"POPL 1995","author":"E.A. Emerson","year":"1995","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: POPL 1995, pp. 85\u201394. ACM, New York (1995)"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-36577-X_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Fontaine","year":"2003","unstructured":"Fontaine, P., Gribomont, E.P.: Decidability of invariant validation for paramaterized systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 97\u2013112. Springer, Heidelberg (2003)"},{"issue":"3","key":"10_CR21","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S.M. German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM\u00a039(3), 675\u2013735 (1992)","journal-title":"J. ACM"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/3-540-46419-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Jonsson","year":"2000","unstructured":"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.\u00a01785, pp. 220\u2013234. Springer, Heidelberg (2000)"},{"key":"10_CR23","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0304-3975(00)00103-1","volume":"256","author":"Y. Kesten","year":"2001","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. Theor. Comput. Sci.\u00a0256, 93\u2013112 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR24","unstructured":"Kofro\u0148, J.: Behavior Protocols Extensions. PhD thesis, Charles University in Prague (2007)"},{"issue":"3","key":"10_CR25","first-page":"219","volume":"2","author":"N.A. Lynch","year":"1989","unstructured":"Lynch, N.A., Tuttle, M.R.: An introduction to input\/output automata. CWI Quarterly\u00a02(3), 219\u2013246 (1989)","journal-title":"CWI Quarterly"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-44585-4_29","volume-title":"Computer Aided Verification","author":"M. Maidl","year":"2001","unstructured":"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.\u00a02102, pp. 311\u2013323. Springer, Heidelberg (2001)"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/3-540-36384-X_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Pnueli","year":"2002","unstructured":"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.\u00a02575, p. 4. Springer, Heidelberg (2002)"},{"key":"10_CR29","unstructured":"Component reliability extensions for fractal component model, http:\/\/kraken.cs.cas.cz\/ft\/public\/public_index.phtml"},{"key":"10_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_32","volume-title":"Computer Aided Verification","author":"T. Rybina","year":"2002","unstructured":"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.\u00a02404. Springer, Heidelberg (2002)"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Va\u0159ekov\u00e1, P., \u010cern\u00e1, 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)","DOI":"10.1007\/978-3-540-87891-9_10"},{"key":"10_CR32","first-page":"3","volume-title":"SAVCBS 2007","author":"P. Va\u0159ekov\u00e1","year":"2007","unstructured":"Va\u0159ekov\u00e1, P., Moravec, P., \u010cern\u00e1, I., Zimmerova, B.: Effective-Verification of Systems with a Dynamic-Number of Components. In: SAVCBS 2007, pp. 3\u201313. ACM Press, New York (2007)"},{"key":"10_CR33","volume-title":"SAVCBS 2007","author":"P. Va\u0159ekov\u00e1","year":"2007","unstructured":"Va\u0159ekov\u00e1, P., Zimmerova, B.: Solution of challenge problem. In: SAVCBS 2007. ACM Press, New York (2007)"},{"key":"10_CR34","unstructured":"Zimmerova, B., Va\u0159ekov\u00e1, P.: Reflecting creation and destruction of instances in CBSs modelling and verification. In: MEMICS 2007, Znojmo, Czech Republic (2007)"},{"key":"10_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-540-85289-6_7","volume-title":"The Common Component Modeling Example: Comparing Software Component Models","author":"B. Zimmerova","year":"2008","unstructured":"Zimmerova, B., Va\u0159ekov\u00e1, P., Bene\u0161, N., \u010cern\u00e1, I., Brim, L., Sochor, J.: Component-Interaction Automata Approach (CoIn). In: PACS 2000. LNCS, vol.\u00a05153, pp. 146\u2013176. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Component-Based Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87891-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T14:11:31Z","timestamp":1557843091000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-87891-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540878902","9783540878919"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87891-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}