{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:48:14Z","timestamp":1742914094533,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642006692"},{"type":"electronic","value":"9783642006708"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-00670-8_16","type":"book-chapter","created":{"date-parts":[[2009,4,2]],"date-time":"2009-04-02T14:15:23Z","timestamp":1238681723000},"page":"213-225","source":"Crossref","is-referenced-by-count":3,"title":["Compositional Model-Checking Verification of Critical Systems"],"prefix":"10.1007","author":[{"given":"Luis E.","family":"Mendoza","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manuel I.","family":"Capel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mar\u00eda","family":"P\u00e9rez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kawtar","family":"Benghazi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"16_CR1","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.: Model checking and modular verification. ACM Transaction on Programming Languages and Systems\u00a016(3), 843\u2013871 (1994)","journal-title":"ACM Transaction on Programming Languages and Systems"},{"issue":"2","key":"16_CR2","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1145\/174662.174665","volume":"16","author":"B. Jonnson","year":"1994","unstructured":"Jonnson, B.: Compositional specification and verification of distributed systems. ACM TOPLAS\u00a016(2), 259\u2013303 (1994)","journal-title":"ACM TOPLAS"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Bultan, T., Fischer, J., Gerber, R.: Compositional verification by model checking for counter\u2013examples. In: ISSTA 1996: Proc. of the 1996 ACM SIGSOFT International Symposium on Software Testing and Analysis (1996)","DOI":"10.1145\/229000.226321"},{"key":"16_CR4","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (2000)"},{"issue":"1","key":"16_CR5","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.scico.2006.08.005","volume":"65","author":"K. Benghazi","year":"2007","unstructured":"Benghazi, K., Capel, M., Holgado, J., Mendoza, L.: A methodological approach to the formal specification of real\u2013time systems by transformation of UML\u2013RT design models. Science of Computer Programming\u00a065(1), 41\u201356 (2007)","journal-title":"Science of Computer Programming"},{"key":"16_CR6","unstructured":"Clarke, E., Long, D., McMillan, K.: Compositional model checking. In: Proc. of the Fourth Annual Symposium on Logic in Computer Science (1989)"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Giese, H., Tichy, M., Burmester, S., Flake, S.: Towards the compositional verification of real\u2013time UML designs. In: ESEC\/FSE\u201311: Proc. 9th European Software Engineering Conference and 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering (2003)","DOI":"10.1145\/940075.940078"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Yeh, W., Young, M.: Compositional reachability analysis using process algebra. In: TAV4: Proc. of the Symposium on Testing, Analysis, and Verification (1991)","DOI":"10.1145\/120807.120812"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/3-540-49213-5_4","volume-title":"Compositionality: The Significant Difference","author":"S. Berezin","year":"1998","unstructured":"Berezin, S., Campos, S., Clarke, E.: Compositional Reasoning in Model Checking. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol.\u00a01536, pp. 81\u2013102. Springer, Heidelberg (1998)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/3-540-48119-2_12","volume-title":"FM\u201999 - Formal Methods","author":"Y. Kesten","year":"1999","unstructured":"Kesten, Y., Klein, A., Pnueli, A., Raanan, G.: A Perfecto Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 173\u2013194. Springer, Heidelberg (1999)"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Cobleigh","year":"2003","unstructured":"Cobleigh, J., Giannakopoulou, D., P\u0103s\u0103reanu, C.: Learning Assumptions for Compositional Verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 331\u2013346. Springer, Heidelberg (2003)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Frehse, G., Stursberg, O., Engell, S., Huuck, R., Lukoschus, B.: Modular analysis of discrete controllers for distributed hybrid systems. In: b 2002: The XV IFAC World Congress, Barcelona, Spain, IFAC, pp. 21\u201326 (2002)","DOI":"10.3182\/20020721-6-ES-1901.00566"},{"key":"16_CR13","unstructured":"Lukoschus, B.: Compositional Verification of Industrial Control Systems: Methods and Case Studies. PhD thesis, Universit\u00e4t zu Kiel, Technischen Fakult\u00e4t der Christian-Albrechts (July 2005)"},{"key":"16_CR14","first-page":"115","volume-title":"SIGSOFT 1993: Proc. of the 1st ACM SIGSOFT Symposium on Foundations of Software Engineering","author":"S. Cheung","year":"1993","unstructured":"Cheung, S., Kramer, J.: Enhancing compositional reachability analysis with context constraints. In: SIGSOFT 1993: Proc. of the 1st ACM SIGSOFT Symposium on Foundations of Software Engineering, pp. 115\u2013125. ACM Press, New York (1993)"},{"key":"16_CR15","unstructured":"Mendoza, L., Capel, M.: Consistency checking of UML composite structure diagrams based on trace semantics. In: Software Engineering in Progress \u2013 2nd IFIP CEE-SET 2007 (2007)"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Mendoza, L., Capel, M., P\u00e9rez, M., Benghazi, K.: A conceptual scheme for compositional model\u2013checking verification of critical communicating systems. In: Proc. 10th ICEIS 2008 ISAS-1, pp. 86\u201393 (June 2008)","DOI":"10.5220\/0001697500860093"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Allen, R., Garlan, D.: A formal basis for architectural connection. ACM Trans. Softw. Eng. Methodol.\u00a06(3) (1997)","DOI":"10.1145\/258077.258078"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Selic, B., Rumbaugh, J.: UML for Modeling Complex Real\u2013Time Systems. ObjecTime Technical Report. ObjecTime, New York, USA (1998)","DOI":"10.1007\/BFb0057795"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/3-540-48153-2_20","volume-title":"Correct Hardware Design and Verification Methods","author":"J. Ruf","year":"1999","unstructured":"Ruf, J., Kropf, T.: Modeling and Checking Networks of Communicating Real-Time Processes. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 256\u2013279. Springer, Heidelberg (1999)"},{"issue":"6","key":"16_CR20","doi-asserted-by":"publisher","first-page":"1661","DOI":"10.1145\/197320.197322","volume":"16","author":"J. \u017dic","year":"1994","unstructured":"\u017dic, J.: Time\u2013constrained buffer specifications in CSP+T and Timed CSP. ACM Transaction on Programming Languages and Systems\u00a016(6), 1661\u20131674 (1994)","journal-title":"ACM Transaction on Programming Languages and Systems"},{"key":"16_CR21","series-title":"International Series in Computer Science","volume-title":"Communicating Sequential Processes","author":"C. Hoare","year":"1985","unstructured":"Hoare, C.: Communicating Sequential Processes. International Series in Computer Science. Prentice\u2013Hall International Ltd., Hertfordshire UK (1985)"},{"key":"16_CR22","unstructured":"Mendoza, L., Capel, M.: Algorithm proposal to automata generation from CCTL formulas. Technical report, University of Granada (2008)"},{"key":"16_CR23","unstructured":"Formal Systems (Europe) Ltd: Failures\u2013Divergence Refinement \u2013 FDR2 User Manual. Formal Systems (Europe) Ltd, Oxford (2005)"}],"container-title":["Lecture Notes in Business Information Processing","Enterprise Information Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00670-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T20:37:56Z","timestamp":1739047076000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00670-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642006692","9783642006708"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00670-8_16","relation":{},"ISSN":["1865-1348","1865-1356"],"issn-type":[{"type":"print","value":"1865-1348"},{"type":"electronic","value":"1865-1356"}],"subject":[],"published":{"date-parts":[[2009]]}}}