{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:49:18Z","timestamp":1750308558649,"version":"3.41.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2015,9,9]],"date-time":"2015-09-09T00:00:00Z","timestamp":1441756800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Academy of Finland projects","award":["139402 and 277522"],"award-info":[{"award-number":["139402 and 277522"]}]},{"name":"SARANA project in the SAFIR 2014 program"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2015,12,8]]},"abstract":"<jats:p>Interface theories (ITs) enable us to analyse the compatibility interfaces and refine them while preserving their compatibility. However, most ITs are for finite state interfaces, whereas computing systems are often parametrised involving components, the number of which cannot be fixed. We present, to our knowledge, the first IT that allows us to specify a parametric number of interfaces. Moreover, we provide a fully algorithmic procedure, implemented in a tool, for checking the compatibility of and refinement between parametrised interfaces. Finally, we show that the restrictions of the technique are necessary; removing any of them renders the refinement checking problem undecidable.<\/jats:p>","DOI":"10.1145\/2776892","type":"journal-article","created":{"date-parts":[[2015,9,15]],"date-time":"2015-09-15T12:09:15Z","timestamp":1442318955000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Parametrised Modal Interface Automata"],"prefix":"10.1145","volume":"14","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9118-5087","authenticated-orcid":false,"given":"Antti","family":"Siirtola","sequence":"first","affiliation":[{"name":"University of Oulu, Oulun yliopisto, Finland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Keijo","family":"Heljanko","sequence":"additional","affiliation":[{"name":"Aalto University, Aalto, Finland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,9,9]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1887654.1887660"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_15"},{"key":"e_1_2_2_4_1","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Approaches to Software Testing","author":"Bijl Machiel","unstructured":"Machiel Bijl, Arend Rensink, and Jan Tretmans. 2004. Compositional testing with IOCO. In Formal Approaches to Software Testing. Lecture Notes in Computer Science, Vol. 2931. Springer, 86--100."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0048-7"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.v38:12"},{"key":"e_1_2_2_7_1","series-title":"Lecture Notes in Computer Science","volume-title":"SOFSEM 2014: Theory and Practice of Computer Science","author":"Bujtor Ferenc","unstructured":"Ferenc Bujtor and Walter Vogler. 2014. Error-pruning in interface automata. In SOFSEM 2014: Theory and Practice of Computer Science. Lecture Notes in Computer Science, Vol. 8327. Springer, 162--173."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1755952.1755967"},{"key":"e_1_2_2_10_1","volume-title":"Henzinger","author":"de Alfaro Luca","year":"2005","unstructured":"Luca de Alfaro and Thomas A. Henzinger. 2005. Interface-based design. In Engineering Theories of Software Intensive Systems. NATO Science Series, Vol. 195. Springer, 83--104."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1450058.1450070"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(4:10)2010"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_55"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1024"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(3:4)2013"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-014-0211-0"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/41840.41852"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2013.09.003"},{"volume-title":"Computational Complexity","author":"Papadimitriou Christos M.","key":"e_1_2_2_20_1","unstructured":"Christos M. Papadimitriou. 1994. Computational Complexity. Addison-Wesley, Reading, MA."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/2362088.2362095"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1941861"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2010.16"},{"key":"e_1_2_2_25_1","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Siirtola Antti","unstructured":"Antti Siirtola. 2014a. Bounds2: A tool for compositional multi-parametrised verification. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, Vol. 8413. Springer, 599--604."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2014.26"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2013.9"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_29"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/645834.670404"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806851"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2776892","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2776892","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:04:01Z","timestamp":1750273441000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2776892"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,9]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,12,8]]}},"alternative-id":["10.1145\/2776892"],"URL":"https:\/\/doi.org\/10.1145\/2776892","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2015,9,9]]},"assertion":[{"value":"2014-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-05-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-09-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}