{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T23:35:39Z","timestamp":1777592139380,"version":"3.51.4"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2016,4,1]],"date-time":"2016-04-01T00:00:00Z","timestamp":1459468800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Architectures depict design principles: paradigms that can be understood by all, allow thinking on a higher plane and avoiding low-level mistakes. They provide means for ensuring correctness by construction by enforcing global properties characterizing the coordination between components. An architecture can be considered as an operator\n            <jats:italic>A<\/jats:italic>\n            that, applied to a set of components\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi mathvariant=\"script\">B<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            , builds a composite component\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>A<\/mml:mi>\n                    <mml:mo stretchy=\"false\">(<\/mml:mo>\n                    <mml:mi mathvariant=\"script\">B<\/mml:mi>\n                    <mml:mo stretchy=\"false\">)<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            meeting a characteristic property\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi mathvariant=\"normal\">\u03a6<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            . Architecture composability is a basic and common problem faced by system designers. In this paper, we propose a formal and general framework for architecture composability based on an associative, commutative and idempotent architecture composition operator\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mo>\u2295<\/mml:mo>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            . The main result is that if two architectures\n            <jats:italic>A<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            and\n            <jats:italic>A<\/jats:italic>\n            <jats:sub>2<\/jats:sub>\n            enforce respectively safety properties\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mi mathvariant=\"normal\">\u03a6<\/mml:mi>\n                    <mml:mn>1<\/mml:mn>\n                  <\/mml:msub>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            and\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mi mathvariant=\"normal\">\u03a6<\/mml:mi>\n                    <mml:mn>2<\/mml:mn>\n                  <\/mml:msub>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            , the architecture\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:msub>\n                      <mml:mi>A<\/mml:mi>\n                      <mml:mn>1<\/mml:mn>\n                    <\/mml:msub>\n                    <mml:mo>\u2295<\/mml:mo>\n                    <mml:msub>\n                      <mml:mi>A<\/mml:mi>\n                      <mml:mn>2<\/mml:mn>\n                    <\/mml:msub>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            enforces the property\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:msub>\n                      <mml:mi mathvariant=\"normal\">\u03a6<\/mml:mi>\n                      <mml:mn>1<\/mml:mn>\n                    <\/mml:msub>\n                    <mml:mo>\u2227<\/mml:mo>\n                    <mml:msub>\n                      <mml:mi mathvariant=\"normal\">\u03a6<\/mml:mi>\n                      <mml:mn>2<\/mml:mn>\n                    <\/mml:msub>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            , that is both properties are preserved by architecture composition. We also establish preservation of liveness properties by architecture composition. The presented results are illustrated by a running example and a case study.\n          <\/jats:p>","DOI":"10.1007\/s00165-015-0349-8","type":"journal-article","created":{"date-parts":[[2015,12,18]],"date-time":"2015-12-18T09:55:37Z","timestamp":1450432537000},"page":"207-231","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["A general framework for architecture composability"],"prefix":"10.1145","volume":"28","author":[{"given":"Paul","family":"Attie","sequence":"first","affiliation":[{"name":"American University of Beirut, Beirut, Lebanon"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eduard","family":"Baranov","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne, Station 14, 1015, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7900-5271","authenticated-orcid":false,"given":"Simon","family":"Bliudze","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne, Station 14, 1015, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamad","family":"Jaber","sequence":"additional","affiliation":[{"name":"American University of Beirut, Beirut, Lebanon"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joseph","family":"Sifakis","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne, Station 14, 1015, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Attie PC Bensalem S Bozga M Jaber M Sifakis J Zaraket FA (2013) An abstract framework for deadlock prevention in BIP. In: FMOODS\/FORTE pp 161\u2013177","DOI":"10.1007\/978-3-642-38592-6_12"},{"key":"e_1_2_1_2_2_2","first-page":"128","volume-title":"12th international conference on software engineering and formal methods (SEFM 2014), LNCS, vol 8702","author":"Attie P","year":"2014"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Attie PC Baranov E Bliudze S Jaber M Sifakis J (2014) A general framework for architecture composability. Technical Report EPFL-REPORT-196536 EPFL IC IIF RiSD. http:\/\/infoscience.epfl.ch\/record\/196536","DOI":"10.1007\/978-3-319-10431-7_10"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151649"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004153"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2011.27"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Bernardo M Ciancarini P Donatiello L (2000) On the formalization of architectural types with process algebras. In: SIGSOFT FSE pp 140\u2013148","DOI":"10.1145\/357474.355064"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.54"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.005"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Bliudze S Sifakis J (2007) The algebra of connectors\u2014structuring interaction in BIP. In: Proceedings of the EMSOFT\u201907 Salzburg. ACM SigBED pp 11\u201320","DOI":"10.1145\/1289927.1289935"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-010-0091-z"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/978-3-642-22045-6_4","volume-title":"Software composition, vol 6708","author":"Bliudze S","year":"2011"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2003.1193228"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1389-1286(02)00352-3"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"D\u2019Souza D Gopinathan M (2008) Conflict-tolerant features. In: CAV LNCS vol 5123. Springer pp 227\u2013239","DOI":"10.1007\/978-3-540-70545-1_22"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Decker G Puhlmann F Weske M (2006) Formalizing service interactions. In: Business process management pp 414\u2013419","DOI":"10.1007\/11841760_32"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805829"},{"key":"e_1_2_1_2_18_2","volume-title":"Interacting processes: a multiparty approach to coordinated distributed programming","author":"Francez N","year":"1996"},{"key":"e_1_2_1_2_19_2","unstructured":"Fiadeiro JL (2004) Categories for Software Engineering. Springer-Verlag"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/357474.355061"},{"key":"e_1_2_1_2_21_2","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice Hall International Series in Computer Science. Prentice Hall"},{"key":"e_1_2_1_2_22_2","unstructured":"Liskov B Guttag J (2000) Program development in java. Addison Wesley"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Li Z Jin Y Han J (2006) A runtime monitoring and validation framework for web service interactions. In: ASWEC pp 70\u201379","DOI":"10.1109\/ASWEC.2006.6"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Liu I Reineke J Lee EA (2010) A PRET architecture supporting concurrent programs with composable timing properties. In: Signals systems and computers (ASILOMAR) 2010 Conference record of the forty fourth asilomar conference pp 2111\u20132115","DOI":"10.1109\/ACSSC.2010.5757922"},{"key":"e_1_2_1_2_25_2","unstructured":"Milner R (1989) Communication and concurrency. Prentice Hall International Series in Computer Science Prentice Hall"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(00)00018-6"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Ray A Cleaveland R (2003) Architectural interaction diagrams: AIDs for system modeling. In: ICSE\u201903: Proceedings of the 25th international conference on software engineering Washington DC. IEEE Computer Society pp 396\u2013406","DOI":"10.1109\/ICSE.2003.1201218"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Spitznagel B Garlan D (2003) A compositional formalization of connector wrappers. In: ICSE. IEEE Computer Society pp 374\u2013384","DOI":"10.1109\/ICSE.2003.1201216"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Sifakis J (2012) Rigorous system design. Found Trends Electron Des Autom 6(4):293\u2013362 2012","DOI":"10.1561\/1000000034"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Wegner P (1996) Coordination as constrained interaction (extended abstract). In: Coordination languages and models LNCS vol 1061. Springer pp 28\u201333","DOI":"10.1007\/3-540-61052-9_37"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-015-0349-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-015-0349-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-015-0349-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:54:56Z","timestamp":1641538496000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-015-0349-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,4]]}},"alternative-id":["10.1007\/s00165-015-0349-8"],"URL":"https:\/\/doi.org\/10.1007\/s00165-015-0349-8","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,4]]}}}