{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:18:29Z","timestamp":1759033109414,"version":"3.41.0"},"reference-count":16,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2005,9,5]],"date-time":"2005-09-05T00:00:00Z","timestamp":1125878400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2006,3]]},"abstract":"<jats:p>\n            In the paper, we present a new approach to component interaction specification and verification process which combines the advantages of both architecture description languages (ADLs) at the beginning of the process, and a general formal verification-oriented model connected to verification tools at the end. After examining current general formal models with respect to their suitability for description of component-based systems, we propose a new verification-oriented model,\n            <jats:italic>Component-Interaction automata<\/jats:italic>\n            , and discuss its features. The model is designed to preserve all the interaction properties to provide a rich base for further verification, and allows the system behaviour to be configurable according to the architecture description (bindings among components) and other specifics (type of communication used in the synchronization of components).\n          <\/jats:p>","DOI":"10.1145\/1118537.1123063","type":"journal-article","created":{"date-parts":[[2006,5,8]],"date-time":"2006-05-08T22:51:53Z","timestamp":1147128713000},"page":"4","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["Component-interaction automata as a verification-oriented component-based system specification"],"prefix":"10.1145","volume":"31","author":[{"given":"Lubo\u0161","family":"Brim","sequence":"first","affiliation":[{"name":"Masaryk University, Brno, Brno, Czech Republic"}]},{"given":"Ivana","family":"\u010cern\u00e1","sequence":"additional","affiliation":[{"name":"Masaryk University, Brno, Brno, Czech Republic"}]},{"given":"Pavl\u00edna","family":"Va\u0159ekov\u00e1","sequence":"additional","affiliation":[{"name":"Masaryk University, Brno, Brno, Czech Republic"}]},{"given":"Barbora","family":"Zimmerova","sequence":"additional","affiliation":[{"name":"Masaryk University, Brno, Brno, Czech Republic"}]}],"member":"320","published-online":{"date-parts":[[2005,9,5]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Divine - Distributed Verification Environment. http:\/\/anna.fi.muni.cz\/divine.  Divine - Distributed Verification Environment. http:\/\/anna.fi.muni.cz\/divine."},{"key":"e_1_2_1_2_1","first-page":"17","volume-title":"Proceedings of the Second International Workshop on Unanticipated Software Evolution (USE 2003","author":"Adamek J.","year":"2003","unstructured":"J. Adamek and F. Plasil . Behavior protocols capturing errors and updates . In Proceedings of the Second International Workshop on Unanticipated Software Evolution (USE 2003 ), ETAPS, pages 17 -- 25 , Warsaw, Poland , April 2003 . University of Warsaw, Poland. J. Adamek and F. Plasil. Behavior protocols capturing errors and updates. In Proceedings of the Second International Workshop on Unanticipated Software Evolution (USE 2003), ETAPS, pages 17--25, Warsaw, Poland, April 2003. University of Warsaw, Poland."},{"key":"e_1_2_1_4_1","volume-title":"Divine - The Distributed Verification Environment. In Proceedings of the Workshop on Parallel and Distributed Methods in verifiCation (PDMC'05)","author":"Barnat J.","year":"2005","unstructured":"J. Barnat , L. Brim , I. \u010cern\u00e1 , and P. \u0160ime\u010dek . Divine - The Distributed Verification Environment. In Proceedings of the Workshop on Parallel and Distributed Methods in verifiCation (PDMC'05) , July 2005 . J. Barnat, L. Brim, I. \u010cern\u00e1, and P. \u0160ime\u010dek. Divine - The Distributed Verification Environment. In Proceedings of the Workshop on Parallel and Distributed Methods in verifiCation (PDMC'05), July 2005."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022407907596"},{"key":"e_1_2_1_6_1","volume-title":"Model Checking","author":"Clarke E. M.","year":"2000","unstructured":"E. M. Clarke , O. Grumberg , and D. A. Peled . Model Checking . The MIT Press , January 2000 . E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, January 2000."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503226"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 2004 Marktoberdorf Summer School","author":"de Alfaro L.","year":"2004","unstructured":"L. de Alfaro and T. A. Henzinger . Interface-based design . In Proceedings of the 2004 Marktoberdorf Summer School . Kluwer , 2004 . L. de Alfaro and T. A. Henzinger. Interface-based design. In Proceedings of the 2004 Marktoberdorf Summer School. Kluwer, 2004."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/266838.267363"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of DIMACS Partial Order Methods Workshop IV","author":"Luckham D. C.","year":"1996","unstructured":"D. C. Luckham . Rapide : A language and toolset for simulation of distributed systems by partial orderings of events . In Proceedings of DIMACS Partial Order Methods Workshop IV , July 1996 . D. C. Luckham. Rapide: A language and toolset for simulation of distributed systems by partial orderings of events. In Proceedings of DIMACS Partial Order Methods Workshop IV, July 1996."},{"key":"e_1_2_1_12_1","volume-title":"Distributed Algorithms","author":"Lynch N.","year":"1996","unstructured":"N. Lynch . Distributed Algorithms . Morgan Kaufmann Publishers , San Mateo, CA , 1996 . N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, San Mateo, CA, 1996."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/41840.41852"},{"issue":"3","key":"e_1_2_1_14_1","first-page":"219","volume":"2","author":"Lynch N. A.","year":"1989","unstructured":"N. A. Lynch and M. R. Tuttle . An introduction to input\/output automata. CWI Quarterly , 2 ( 3 ): 219 -- 246 , September 1989 . N. A. Lynch and M. R. Tuttle. An introduction to input\/output automata. CWI Quarterly, 2(3):219--246, September 1989.","journal-title":"An introduction to input\/output automata. CWI Quarterly"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/645385.651497"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/646545.696373"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2002.1049404"},{"key":"e_1_2_1_18_1","volume-title":"Hierarchical correctness proofs for distributed algorithms. Master's thesis","author":"Tuttle M. R.","year":"1987","unstructured":"M. R. Tuttle . Hierarchical correctness proofs for distributed algorithms. Master's thesis , Massachusetts Institute of Technology , Laboratory for Computer Science, April 1987 . M. R. Tuttle. Hierarchical correctness proofs for distributed algorithms. Master's thesis, Massachusetts Institute of Technology, Laboratory for Computer Science, April 1987."}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1118537.1123063","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1118537.1123063","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:08:18Z","timestamp":1750262898000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1118537.1123063"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,9,5]]},"references-count":16,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2006,3]]}},"alternative-id":["10.1145\/1118537.1123063"],"URL":"https:\/\/doi.org\/10.1145\/1118537.1123063","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1123058.1123063","asserted-by":"subject"}]},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2005,9,5]]},"assertion":[{"value":"2005-09-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}