{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T14:49:06Z","timestamp":1773326946838,"version":"3.50.1"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2013,7,1]],"date-time":"2013-07-01T00:00:00Z","timestamp":1372636800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2013,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Component-based development is a well-established methodology of software development. Nevertheless, some of the benefits that the component based development offers are often neglected. One of them is modeling and subsequent analysis of component behavior, which can help establish correctness guarantees, such as absence of composition errors and safety of component updates. We believe that application of component behavior modeling in practice is limited due to huge differences between the behavior modeling languages (e.g., process algebras) and the common implementation languages (e.g., Java). As a result, many concepts of the implementation languages are either very different or completely missing in the behavior modeling languages. As an example, even though behavior modeling languages are practical for modeling and analysis of various message-based protocols, they are not well suited for modeling current component applications, where thread-based parallelism, lock-based synchronization, and nested method calls are the essential building blocks. With this in mind, we propose a new behavior modeling language for software components, Threaded Behavior Protocols (TBP). At the model level, TBP provides developers with the concepts known from the implementation languages and essential to most component applications. In addition, the theoretical framework of TBP provides a notion of correctness based on absence of communication errors and a refinement relation to verify correctness of hierarchical components. The main asset of TBP formalism is that it links together the notion of threads as used in imperative object oriented languages and the notion of refinement. For instance, this allows reasoning about hierarchical components composed of primitive components implemented in Java without the need of bridging abstractions and simplifications enforced by the modeling languages.<\/jats:p>","DOI":"10.1007\/s00165-011-0194-3","type":"journal-article","created":{"date-parts":[[2011,9,17]],"date-time":"2011-09-17T07:12:41Z","timestamp":1316243561000},"page":"543-572","source":"Crossref","is-referenced-by-count":1,"title":["Threaded behavior protocols"],"prefix":"10.1145","volume":"25","author":[{"given":"Tom\u00e1\u0161","family":"Poch","sequence":"first","affiliation":[{"name":"Faculty of Mathematics and Physics, Charles University Prague, Malostransk\u00e9 n\u00e1m\u011bst\u00ed 25, 118 00, Prague 1, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ond\u0159ej","family":"\u0160er\u00fd","sequence":"additional","affiliation":[{"name":"Faculty of Mathematics and Physics, Charles University Prague, Malostransk\u00e9 n\u00e1m\u011bst\u00ed 25, 118 00, Prague 1, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franti\u0161ek","family":"Pl\u00e1\u0161il","sequence":"additional","affiliation":[{"name":"Faculty of Mathematics and Physics, Charles University Prague, Malostransk\u00e9 n\u00e1m\u011bst\u00ed 25, 118 00, Prague 1, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Kofro\u0148","sequence":"additional","affiliation":[{"name":"Faculty of Mathematics and Physics, Charles University Prague, Malostransk\u00e9 n\u00e1m\u011bst\u00ed 25, 118 00, Prague 1, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-84800-223-4","volume-title":"A process algebraic approach to software architecture design","author":"Aldini A","year":"2010"},{"key":"e_1_2_1_2_2_2","unstructured":"Adamek J Bures T Jezek P Kofron J Mencl V Parizek P Plasil F (2006) Component reliability extensions for fractal component model. \nhttp:\/\/kraken.cs.cas.cz\/ft\/public\/public_index.phtml"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/503271.503226"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"de Alfaro L Henzinger TA (2001) Interface theories for component-based design. In: EMSOFT \u201901: Proceedings of the first international workshop on embedded software. London UK Springer Berlin pp 148\u2013165","DOI":"10.1007\/3-540-45449-7_11"},{"key":"e_1_2_1_2_5_2","unstructured":"Allen RJ (1997) A formal approach to software architecture. PhD thesis CMU"},{"key":"e_1_2_1_2_6_2","unstructured":"Adamek J Plasil F (2003) Behavior protocols capturing errors and updates. In: Proceedings of the 2nd international workshop on unanticipated software evolution"},{"issue":"5","key":"e_1_2_1_2_7_2","first-page":"102","article-title":"Component composition errors and update atomicity: Static analysis","volume":"17","author":"Adamek J","year":"2004","journal-title":"J Softw Maint Evol Res Pract"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Basu A Bozga M Sifakis J (2006) Modeling heterogeneous real-time components in bip. In: Proceedings of the fourth IEEE international conference on software engineering and formal methods Washington DC USA. IEEE Computer Society pp 3\u201312","DOI":"10.1109\/SEFM.2006.27"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bure\u0161 T D\u011bck\u00fd M Hn\u011btynka P Kofro\u0148 J Par\u00edzek P Pl\u00e1\u0161il F Poch T \u0160er\u00fd O T\u016fma P (2008) CoCoME in SOFA. In: The common component modeling example: comparing software component models. Springer Berlin pp 388\u2013417","DOI":"10.1007\/978-3-540-85289-6_15"},{"key":"e_1_2_1_2_10_2","unstructured":"Badger\u2014Verification of component behavior specification. http:\/\/d3s.mff.cuni.cz\/~sery\/badger"},{"key":"e_1_2_1_2_11_2","unstructured":"Booch G Rumbaugh J Jacobson I (2005) Unified modeling language user guide 2nd edn. Addison-Wesley Object Technology Series. Addison-Wesley Professional"},{"key":"e_1_2_1_2_12_2","unstructured":"Modelling Contest: Common Component Modelling Example. http:\/\/agrausch.informatik.uni-kl.de\/CoCoME"},{"key":"e_1_2_1_2_13_2","first-page":"243","volume-title":"Lecture notes in computer science, vol 4111","author":"Clarke EM","year":"2005"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"\u010cern\u00e1 I Va\u0159ekov\u00e1 P Zimmerova B (2007) Component substitutability via equivalencies of component-interaction automata. In: Proceedings of the workshop on formal aspects of component software (FACS\u201906). ENTCS vol 182. Elsevier Science Publishers pp 39\u201355 June 2007","DOI":"10.1016\/j.entcs.2006.09.030"},{"key":"e_1_2_1_2_15_2","first-page":"242","volume-title":"Proceedings of 16th international conference on computer aided verification (CAV 2004), Boston, MA, USA, July 13\u201317, 2004 Lecture notes in computer science, vol 3114","author":"Fournet C","year":"2004"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Fournet C Hoare T Rajamani SK Rehof J (2004) Stuck-free conformance theory for ccs. Technical report Microsoft Research July 2004","DOI":"10.1007\/978-3-540-27813-9_19"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.5555\/549076"},{"key":"e_1_2_1_2_18_2","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice Hall International (UK) Ltd"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050043"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Kofron J (2007) Checking software component behavior using behavior protocols and spin. In: Proceedings of applied computing 2007 Seoul Korea pp 1513\u20131517","DOI":"10.1145\/1244002.1244326"},{"key":"e_1_2_1_2_21_2","first-page":"64","volume-title":"ESOP. Lecture notes in computer science, vol 4421","author":"Larsen KG","year":"2007"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.5555\/336431"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Magee J Dulay N Eisenbach S Kramer J (1995) Specifying distributed software architectures. In: Fifth European software engineering conference ESEC \u201995 Barcelona","DOI":"10.1007\/3-540-60406-5_12"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/225494"},{"key":"e_1_2_1_2_25_2","unstructured":"Matena V Stearns B Demichiel L (2003) Applying enterprise JavaBeans: component-based development for the J2EE platform. Pearson Education"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.825699"},{"key":"e_1_2_1_2_27_2","unstructured":"OMG Group (2006) CORBA component model specification. Technical report OMG Group"},{"key":"e_1_2_1_2_28_2","unstructured":"Poch T (2010) Towards thread aware component behavior specifications. PhD thesis Charles University Prague"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Plasil F Visnovsky S (2002) Behavior protocols for software components. IEEE Trans Softw Eng 28(9)","DOI":"10.1109\/TSE.2002.1049404"},{"key":"e_1_2_1_2_30_2","unstructured":"Roscoe AW (1998) The theory and practice of concurrency. Prentice Hall"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Rausch A Reussner R Mirandola R Plasil F (eds) (2008) The common component modeling example: comparing software component models. In: Lecture notes in computer science vol 5153. Springer Berlin","DOI":"10.1007\/978-3-540-85289-6"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0194-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-011-0194-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0194-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:56:06Z","timestamp":1641484566000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0194-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7]]},"references-count":31,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,7]]}},"alternative-id":["10.1007\/s00165-011-0194-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0194-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7]]}}}