{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,24]],"date-time":"2026-06-24T15:33:25Z","timestamp":1782315205944,"version":"3.54.5"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031198489","type":"print"},{"value":"9783031198496","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-19849-6_12","type":"book-chapter","created":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T15:03:32Z","timestamp":1666191812000},"page":"188-204","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Twinning-by-Construction: Ensuring Correctness for\u00a0Self-adaptive Digital Twins"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0996-2543","authenticated-orcid":false,"given":"Eduard","family":"Kamburjan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3588-5609","authenticated-orcid":false,"given":"Crystal Chang","family":"Din","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5601-5517","authenticated-orcid":false,"given":"Rudolf","family":"Schlatte","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9948-2748","authenticated-orcid":false,"given":"S. Lizeth Tapia","family":"Tarifa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5382-3949","authenticated-orcid":false,"given":"Einar Broch","family":"Johnsen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,10,17]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-642-02161-9_3","volume-title":"Software Engineering for Self-Adaptive Systems","author":"Y Brun","year":"2009","unstructured":"Brun, Y., et al.: Engineering self-adaptive systems through feedback loops. In: Cheng, B.H.C., de Lemos, R., Giese, H., Inverardi, P., Magee, J. (eds.) Software Engineering for Self-Adaptive Systems. LNCS, vol. 5525, pp. 48\u201370. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02161-9_3"},{"issue":"1","key":"12_CR2","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/MC.2003.1160055","volume":"36","author":"JO Kephart","year":"2003","unstructured":"Kephart, J.O., Chess, D.M.: The vision of autonomic computing. Computer 36(1), 41\u201350 (2003)","journal-title":"Computer"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Riccobene, E., Scandurra, P.: Modeling and analyzing MAPE-K feedback loops for self-adaptation. In: Inverardi, P., Schmerl, B.R. (eds.) 10th IEEE\/ACM International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2015), pp. 13\u201323. IEEE Computer Society (2015)","DOI":"10.1109\/SEAMS.2015.10"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-030-77385-4_8","volume-title":"The Semantic Web","author":"E Kamburjan","year":"2021","unstructured":"Kamburjan, E., Klungre, V.N., Schlatte, R., Johnsen, E.B., Giese, M.: Programming and debugging with semantically lifted states. In: Verborgh, R., et al. (eds.) ESWC 2021. LNCS, vol. 12731, pp. 126\u2013142. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-77385-4_8"},{"key":"12_CR5","unstructured":"Blochwitz, T., et al.: Functional mockup interface 2.0: the standard for tool independent exchange of simulation models. In: The Modelica Association Modelica Conference, pp. 173\u2013184 (2012)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Kamburjan, E., Johnsen, E.B.: Knowledge structures over simulation units. In: Proceedings of the SCS Annual Modeling and Simulation Conference (ANNSIM) (2022). In press","DOI":"10.23919\/ANNSIM55834.2022.9859490"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Kamburjan, E., Klungre, V.N., Schlatte, R., Tapia Tarifa, S.L., Cameron, D., Johnsen, E.B.: Digital twin reconfiguration using asset models. In: Proceedings of the 11th International Symposium on Leveraging Applications of Formal Methods (ISoLA 2022) (2022). This volume","DOI":"10.1007\/978-3-031-19762-8_6"},{"key":"12_CR8","unstructured":"Gould, L.S.: What are digital twins and digital threads? Automot. Des. Prod. 23 (2018)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-34968-4_1","volume-title":"Integrated Formal Methods","author":"T Margaria","year":"2019","unstructured":"Margaria, T., Schieweck, A.: The digital thread in industry 4.0. In: Ahrendt, W., Tapia Tarifa, S.L. (eds.) IFM 2019. LNCS, vol. 11918, pp. 3\u201324. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-34968-4_1"},{"key":"12_CR10","volume-title":"Foundations of Semantic Web Technologies","author":"P Hitzler","year":"2010","unstructured":"Hitzler, P., Kr\u00f6tzsch, M., Rudolph, S.: Foundations of Semantic Web Technologies. CRC Press, Chapman and Hall (2010)"},{"key":"12_CR11","unstructured":"W3C, RDF Working Group: Resource description framework https:\/\/www.w3.org\/RDF"},{"key":"12_CR12","unstructured":"Fjosna, E., Waaler, A.: READI information modelling framework (IMF). Asset Information Modelling Framework. Technical report, READI Joint Industry Project (2021). https:\/\/readi-jip.org\/wp-content\/uploads\/2021\/03\/Information-modelling-framework-V1.pdf"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35813-5_1","volume-title":"Software Engineering for Self-Adaptive Systems II","author":"R de Lemos","year":"2013","unstructured":"de Lemos, R., et al.: Software engineering for self-adaptive systems: a second research roadmap. In: de Lemos, R., Giese, H., M\u00fcller, H.A., Shaw, M. (eds.) Software Engineering for Self-Adaptive Systems II. LNCS, vol. 7475, pp. 1\u201332. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35813-5_1"},{"issue":"6","key":"12_CR14","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"issue":"11","key":"12_CR15","doi-asserted-by":"publisher","first-page":"1016","DOI":"10.1016\/j.ifacol.2018.08.474","volume":"51","author":"W Kritzinger","year":"2018","unstructured":"Kritzinger, W., Karner, M., Traar, G., Henjes, J., Sihn, W.: Digital twin in manufacturing: a categorical literature review and classification. IFAC-PapersOnLine 51(11), 1016\u20131022 (2018)","journal-title":"IFAC-PapersOnLine"},{"key":"12_CR16","unstructured":"W3C, SPARQL Working Group: Sparql 1.1 query language https:\/\/www.w3.org\/TR\/sparq"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Brandt, S., Kalayci, E.G., Kontchakov, R., Ryzhikov, V., Xiao, G., Zakharyaschev, M.: Ontology-based data access with a horn fragment of metric temporal logic. In: AAAI, pp. 1070\u20131076, AAAI Press (2017)","DOI":"10.1609\/aaai.v31i1.10696"},{"issue":"4","key":"12_CR18","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real Time Syst. 2(4), 255\u2013299 (1990)","journal-title":"Real Time Syst."},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-319-11164-3_15","volume-title":"Runtime Verification","author":"H-M Ho","year":"2014","unstructured":"Ho, H.-M., Ouaknine, J., Worrell, J.: Online monitoring of metric temporal logic. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 178\u2013192. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_15"},{"key":"12_CR20","doi-asserted-by":"publisher","first-page":"41805","DOI":"10.1109\/ACCESS.2020.2977136","volume":"8","author":"H Yan","year":"2020","unstructured":"Yan, H., Yang, J., Wan, J.: KnowIME: a system to construct a knowledge graph for intelligent manufacturing equipment. IEEE Access 8, 41805\u201341813 (2020)","journal-title":"IEEE Access"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Banerjee, A., Dalal, R., Mittal, S., Joshi, K.P.: Generating digital twin models using knowledge graphs for industrial production lines. In: Proceedings of the Web Science Conference (WebSci 2017), pp. 425\u2013430, ACM (2017)","DOI":"10.1145\/3091478.3162383"},{"key":"12_CR22","unstructured":"Oakes, B.J., Meyers, B., Janssens, D., Vangheluwe, H.: Structuring and accessing knowledge for historical and streaming digital twins. In: Tiddi, I., Maleshkova, M., Pellegrini, T., de Boer, V., (eds.) Joint Proceedings of the Semantics Co-located Events: Poster & Demo Track and Workshop on Ontology-Driven Conceptual Modelling of Digital Twins Co-located with Semantics 2021, vol. 2941 of CEUR Workshop Proceedings. CEUR-WS.org (2021)"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Waszak, M., Lam, A.N., Hoffmann, V., Elves\u00e6ter, B., Mogos, M.F., Roman, D.: Let the asset decide: digital twins with knowledge graphs. In: 19th IEEE International Conference on Software Architecture (ICSA) (2022)","DOI":"10.1109\/ICSA-C54293.2022.00014"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Kharlamov, E., Mart\u00edn-Recuerda, F., Perry, B., Cameron, D., Fjellheim, R., Waaler, A.: Towards semantically enhanced digital twins. In: IEEE BigData, pp. 4189\u20134193, IEEE (2018)","DOI":"10.1109\/BigData.2018.8622503"},{"key":"12_CR25","doi-asserted-by":"publisher","DOI":"10.1016\/j.websem.2021.100664","volume":"71","author":"B Zhou","year":"2021","unstructured":"Zhou, B., et al.: SemML: facilitating development of ML models for condition monitoring with semantics. J. Web Semant. 71, 100664 (2021)","journal-title":"J. Web Semant."},{"key":"12_CR26","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-030-85874-2_26","volume-title":"Advances in Production Management Systems. Artificial Intelligence for Sustainable and Resilient Production Systems","author":"P Lietaert","year":"2021","unstructured":"Lietaert, P., Meyers, B., Van Noten, J., Sips, J., Gadeyne, K.: Knowledge graphs in digital twins for AI in production. In: Dolgui, A., Bernard, A., Lemoine, D., von Cieminski, G., Romero, D. (eds.) APMS 2021. IAICT, vol. 630, pp. 249\u2013257. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85874-2_26"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-030-83723-5_6","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends","author":"J Woodcock","year":"2021","unstructured":"Woodcock, J., Gomes, C., Macedo, H.D., Larsen, P.G.: Uncertainty quantification and runtime monitoring using environment-aware digital twins. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12479, pp. 72\u201387. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-83723-5_6"},{"issue":"1","key":"12_CR28","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10703-017-0286-7","volume":"51","author":"JV Deshmukh","year":"2017","unstructured":"Deshmukh, J.V., Donz\u00e9, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. Form. Methods Syst. Des. 51(1), 5\u201330 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0286-7","journal-title":"Form. Methods Syst. Des."},{"key":"12_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-319-74183-3_2","volume-title":"Software Engineering for Self-Adaptive Systems III. Assurances","author":"D Weyns","year":"2017","unstructured":"Weyns, D., et al.: Perpetual assurances for self-adaptive systems. In: de Lemos, R., Garlan, D., Ghezzi, C., Giese, H. (eds.) Software Engineering for Self-Adaptive Systems III. Assurances. LNCS, vol. 9640, pp. 31\u201363. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-74183-3_2"},{"issue":"11","key":"12_CR30","doi-asserted-by":"publisher","first-page":"1039","DOI":"10.1109\/TSE.2017.2738640","volume":"44","author":"R Calinescu","year":"2017","unstructured":"Calinescu, R., Weyns, D., Gerasimou, S., Iftikhar, M.U., Habli, I., Kelly, T.: Engineering trustworthy self-adaptive software with dynamic assurance cases. IEEE Trans. Softw. Eng. 44(11), 1039\u20131069 (2017)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"12_CR31","doi-asserted-by":"crossref","unstructured":"Iftikhar, M.U., Weyns, D.: ActivFORMS: active formal models for self-adaptation. In: Proceedings of the 9th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2014), pp. 125\u2013134, ACM (2014)","DOI":"10.1145\/2593929.2593944"},{"key":"12_CR32","doi-asserted-by":"publisher","first-page":"34790","DOI":"10.1109\/ACCESS.2018.2849821","volume":"6","author":"MI Fakhir","year":"2018","unstructured":"Fakhir, M.I., Kazmi, S.A.R.: Formal specification and verification of self-adaptive concurrent systems. IEEE Access 6, 34790\u201334803 (2018)","journal-title":"IEEE Access"},{"key":"12_CR33","first-page":"6","volume":"17","author":"NA Mian","year":"2017","unstructured":"Mian, N.A., Ahmad, F.: Modeling and analysis of MAPE-K loop in self adaptive systems using Petri nets. Int. J. Comput. Sci. Netw. Secur. 17, 6 (2017)","journal-title":"Int. J. Comput. Sci. Netw. Secur."},{"issue":"4","key":"12_CR34","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1007\/s10626-021-00343-3","volume":"31","author":"M Camilli","year":"2021","unstructured":"Camilli, M., Capra, L.: Formal specification and verification of decentralized self-adaptive systems using symmetric nets. Discrete Event Dyn. Syst. 31(4), 609\u2013657 (2021)","journal-title":"Discrete Event Dyn. Syst."},{"key":"12_CR35","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Riccobene, E., Scandurra, P.: Formal design and verification of self-adaptive systems with decentralized control. In: ACM Transactions on Autonomous and Adaptive Systems (2016)","DOI":"10.1145\/3019598"},{"key":"12_CR36","doi-asserted-by":"crossref","unstructured":"Feng, H., et al.: Integration of the MAPE-K loop into digital twins ANNSIM (2022). To appear","DOI":"10.23919\/ANNSIM55834.2022.9859489"},{"key":"12_CR37","doi-asserted-by":"crossref","unstructured":"P\u00e4\u00dfler, J., Aguado, E., Silva, G.R., Corbato, C.H., Johnsen, E.B., Tapia Tarifa, S.L.: A formal model of Metacontrol in Maude (2022). Under review","DOI":"10.1007\/978-3-031-19849-6_32"},{"key":"12_CR38","unstructured":"Corbato, C.H.: Model-based self-awareness patterns for autonomy. PhD thesis, Universidad Polit\u00e9cnica de Madrid (2013)"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-19849-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,20]],"date-time":"2022-10-20T00:08:08Z","timestamp":1666224488000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-19849-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031198489","9783031198496"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-19849-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"17 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}