{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:25:31Z","timestamp":1740108331758,"version":"3.37.3"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2021,8,30]],"date-time":"2021-08-30T00:00:00Z","timestamp":1630281600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,8,30]],"date-time":"2021-08-30T00:00:00Z","timestamp":1630281600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["VO 615\/12-2","LU 1748\/3-2"],"award-info":[{"award-number":["VO 615\/12-2","LU 1748\/3-2"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2022,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Interface theories based on <jats:italic>Interface Automata<\/jats:italic> (IA) are formalisms for the component-based specification of concurrent systems. Extensions of their basic synchronization mechanism permit the modelling of data, but are studied in more complex settings involving modal transition systems or do not abstract from internal computation. In this article, we show how de\u00a0Alfaro and Henzinger\u2019s original IA theory can be conservatively extended by shared memory data, without sacrificing simplicity or imposing restrictions. Our extension <jats:italic>IA for shared Memory<\/jats:italic> (IAM) decorates transitions with pre- and post-conditions over algebraic expressions on shared variables, which are taken into account by IA\u2019s notion of component compatibility. Simplicity is preserved as IAM can be embedded into IA and, thus, accurately lifts IA\u2019s compatibility concept to shared memory. We also provide a ground semantics for IAM that demonstrates that our abstract handling of data within IA\u2019s open systems view is faithful to the standard treatment of data in closed systems.<\/jats:p>","DOI":"10.1007\/s00236-021-00408-8","type":"journal-article","created":{"date-parts":[[2021,8,30]],"date-time":"2021-08-30T19:02:35Z","timestamp":1630350155000},"page":"521-556","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Interface Automata for Shared Memory"],"prefix":"10.1007","volume":"59","author":[{"given":"Ayleen","family":"Schinko","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Walter","family":"Vogler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Johannes","family":"Gareis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"N. Tri","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0925-4870","authenticated-orcid":false,"given":"Gerald","family":"L\u00fcttgen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,8,30]]},"reference":[{"key":"408_CR1","doi-asserted-by":"crossref","unstructured":"Bauer, S.S., Hennicker, R., Bidoit, M.: A modal interface theory with data constraints. In: SBMF, volume 6527 of LNCS, pp. 80\u201395. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-19829-8_6"},{"issue":"28","key":"408_CR2","doi-asserted-by":"publisher","first-page":"3101","DOI":"10.1016\/j.tcs.2011.04.007","volume":"412","author":"SS Bauer","year":"2011","unstructured":"Bauer, S.S., Hennicker, R., Wirsing, M.: Interface theories for concurrency and data. Theoret. Comput. Sci. 412(28), 3101\u20133121 (2011)","journal-title":"Theoret. Comput. Sci."},{"key":"408_CR3","doi-asserted-by":"crossref","unstructured":"Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R.: On weak modal compatibility, refinement, and the MIO Workbench. In: TACAS, volume 6015 of LNCS, pp. 175\u2013189. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-12002-2_15"},{"issue":"2\u20133","key":"408_CR4","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1561\/1000000053","volume":"12","author":"A Benveniste","year":"2018","unstructured":"Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.-B., Reinkemeier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T.A., Larsen, K.G.: Contracts for system design. Found. Trends Electr. Des. Autom. 12(2\u20133), 124\u2013400 (2018)","journal-title":"Found. Trends Electr. Des. Autom."},{"issue":"C","key":"408_CR5","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1016\/j.tcs.2016.06.011","volume":"642","author":"F Bujtor","year":"2016","unstructured":"Bujtor, F., Fendrich, S., L\u00fcttgen, G., Vogler, W.: Nondeterministic modal interfaces. Theoret. Comput. Sci. 642(C), 24\u201353 (2016)","journal-title":"Theoret. Comput. Sci."},{"key":"408_CR6","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1016\/j.tcs.2015.06.047","volume":"597","author":"F Bujtor","year":"2015","unstructured":"Bujtor, F., Vogler, W.: Error-pruning in interface automata. Theoret. Comput. Sci. 597, 18\u201339 (2015)","journal-title":"Theoret. Comput. Sci."},{"key":"408_CR7","doi-asserted-by":"crossref","unstructured":"Bunte, O., Groote, J.F., Keiren, J.J.A., Laveaux, M., Neele, T., de Vink, E.P., Wesselink, W., Wijs, A., Willemse, T.A.C.: The mCRL2 toolset for analysing concurrent systems\u2013improvements in expressivity and usability. In: TACAS, volume 11428 of LNCS, pp. 21\u201339. Springer, Berlin (2019)","DOI":"10.1007\/978-3-030-17465-1_2"},{"key":"408_CR8","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1016\/j.tcs.2014.07.018","volume":"549","author":"C Chilton","year":"2014","unstructured":"Chilton, C., Jonsson, B., Kwiatkowska, M.: An algebraic theory of interface automata. Theoret. Comput. Sci. 549, 146\u2013174 (2014)","journal-title":"Theoret. Comput. Sci."},{"issue":"6","key":"408_CR9","first-page":"3","volume":"238","author":"S Chouali","year":"2010","unstructured":"Chouali, S., Mountassir, H., Mouelhi, S.: An I\/O automata-based approach to verify component compatibility: application to the CyCab car. ENTCS 238(6), 3\u201313 (2010)","journal-title":"ENTCS"},{"key":"408_CR10","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.ic.2017.06.002","volume":"256","author":"O Dardha","year":"2017","unstructured":"Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. Inf. Comput. 256, 253\u2013286 (2017)","journal-title":"Inf. Comput."},{"key":"408_CR11","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., da Silva, L.D., Faella, M., Legay, A., Roy, P., Sorea, M.: Sociable interfaces. In: FroCoS, volume 3717 of LNCS, pp. 81\u2013105. Springer, Berlin (2005)","DOI":"10.1007\/11559306_5"},{"key":"408_CR12","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC\/FSE, pp. 109\u2013120. ACM (2001)","DOI":"10.1145\/503271.503226"},{"key":"408_CR13","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface-based design. In: ETSIS, volume 195 of NAII, pp. 83\u2013104. Springer, Berlin (2005)","DOI":"10.1007\/1-4020-3532-2_3"},{"key":"408_CR14","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/6874.001.0001","volume-title":"Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits","author":"DL Dill","year":"1989","unstructured":"Dill, D.L.: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT Press, Cambridge (1989)"},{"issue":"4","key":"408_CR15","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/s00236-018-0319-8","volume":"56","author":"S Fendrich","year":"2019","unstructured":"Fendrich, S., L\u00fcttgen, G.: A generalised theory of interface automata, component compatibility and error. Acta Inf. 56(4), 298\u2013319 (2019)","journal-title":"Acta Inf."},{"key":"408_CR16","doi-asserted-by":"crossref","unstructured":"Gareis, J., L\u00fcttgen, G., Schinko, A., Vogler, W.: Interface automata for shared memory. In: Models, Mindsets, Meta: The What, the How, and the Why Not?\u2014Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday, volume 11200 of LNCS, pp. 151\u2013166. Springer, Berlin (2018)","DOI":"10.1007\/978-3-030-22348-9_10"},{"issue":"3","key":"408_CR17","doi-asserted-by":"publisher","first-page":"16:1","DOI":"10.1145\/2187671.2187678","volume":"44","author":"J Hatcliff","year":"2012","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1-16:58 (2012)","journal-title":"ACM Comput. Surv."},{"key":"408_CR18","doi-asserted-by":"crossref","unstructured":"Holik, L., Isberner, M., Jonsson, B.: Mediator synthesis in a component algebra with data. In: Correct System Design, volume 9360 of LNCS, pp. 238\u2013259. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-23506-6_16"},{"issue":"1","key":"408_CR19","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/1328897.1328472","volume":"43","author":"K Honda","year":"2008","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. SIGPLAN Not. 43(1), 273\u2013284 (2008)","journal-title":"SIGPLAN Not."},{"issue":"1","key":"408_CR20","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"PC Kanellakis","year":"1990","unstructured":"Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43\u201368 (1990)","journal-title":"Inf. Comput."},{"key":"408_CR21","doi-asserted-by":"crossref","unstructured":"Larsen, K.G.: Modal specifications. In: Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, pp. 232\u2013246. Springer, Berlin (1989)","DOI":"10.1007\/3-540-52148-8_19"},{"key":"408_CR22","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Nyman, U., Wasowski, A.: Modal I\/O automata for interface and product line theories. In: ESOP, volume 4421 of LNCS, pp. 64\u201379. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-71316-6_6"},{"issue":"3:4","key":"408_CR23","first-page":"1","volume":"9","author":"G L\u00fcttgen","year":"2013","unstructured":"L\u00fcttgen, G., Vogler, W.: Modal interface automata. Log. Methods Comput. Sci. 9(3:4), 1\u201328 (2013)","journal-title":"Log. Methods Comput. Sci."},{"key":"408_CR24","doi-asserted-by":"crossref","unstructured":"Mateescu, R., Oudot, E.: Improved on-the-fly equivalence checking using boolean equation systems. In: SPIN, volume 5156 of LNCS, pp. 196\u2013213. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-85114-1_15"},{"key":"408_CR25","doi-asserted-by":"crossref","unstructured":"Meyer, B.: Applying \u201cDesign by Contract\u201d. IEEE Comput. 25(10), 40\u201351 (1992)","DOI":"10.1109\/2.161279"},{"key":"408_CR26","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)"},{"issue":"1","key":"408_CR27","first-page":"111","volume":"253","author":"S Mouelhi","year":"2009","unstructured":"Mouelhi, S., Chouali, S., Mountassir, H.: Refinement of interface automata strengthened by action semantics. ENTCS 253(1), 111\u2013126 (2009)","journal-title":"ENTCS"},{"key":"408_CR28","unstructured":"Nguyen, N.T., L\u00fcttgen, G. The IAM Toolset, 2021. Available at GitHub: https:\/\/github.com\/uniba-swt\/ia-toolset"},{"issue":"1\u20132","key":"408_CR29","doi-asserted-by":"publisher","first-page":"119","DOI":"10.3233\/FI-2011-416","volume":"108","author":"J-B Raclet","year":"2011","unstructured":"Raclet, J.-B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fundam. Inform. 108(1\u20132), 119\u2013149 (2011)","journal-title":"Fundam. Inform."},{"key":"408_CR30","first-page":"289","volume":"28","author":"A Schinko","year":"2018","unstructured":"Schinko, A., Vogler, W.: Fault-free refinements for interface automata. Sci. Ann. Comp. Sci. 28, 289\u2013337 (2018)","journal-title":"Sci. Ann. Comp. Sci."},{"issue":"3","key":"408_CR31","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/s00236-020-00369-4","volume":"57","author":"W Vogler","year":"2020","unstructured":"Vogler, W., L\u00fcttgen, G.: A linear-time branching-time perspective on interface automata. Acta Inform. 57(3), 513\u2013550 (2020)","journal-title":"Acta Inform."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-021-00408-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-021-00408-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-021-00408-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,24]],"date-time":"2022-09-24T09:02:45Z","timestamp":1664010165000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-021-00408-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,30]]},"references-count":31,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2022,10]]}},"alternative-id":["408"],"URL":"https:\/\/doi.org\/10.1007\/s00236-021-00408-8","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2021,8,30]]},"assertion":[{"value":"28 November 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 July 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 August 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}