{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T13:49:55Z","timestamp":1777902595421,"version":"3.51.4"},"reference-count":55,"publisher":"SAGE Publications","issue":"5","license":[{"start":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T00:00:00Z","timestamp":1721865600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"},{"start":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T00:00:00Z","timestamp":1721865600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101089047"],"award-info":[{"award-number":["101089047"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/V026801\/2"],"award-info":[{"award-number":["EP\/V026801\/2"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/V043676\/1"],"award-info":[{"award-number":["EP\/V043676\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["101070802"],"award-info":[{"award-number":["101070802"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["SIMULATION"],"published-print":{"date-parts":[[2025,5]]},"abstract":"<jats:p>\n                    Digital twin is a technology that facilitates a real-time coupling of a cyber\u2013physical system and its virtual representation. The technology is applicable to a variety of domains and facilitates more intelligent and dependable system design and operation, but it relies heavily on the existence of digital models that can be depended upon. In realistic systems, there is no single monolithic digital model of the system. Instead, the system is broken into subsystems, with models exported from different tools corresponding to each subsystem. In this paper, we focus on techniques that can be used for a black-box model, such as the ones implementing the Functional Mock-up Interface (FMI) standard, formal analysis, and verification. We propose two techniques for simulation-based reachability analysis of models. The first one is based on system dynamics, while the second one utilizes dynamic sensitivity analysis to improve the quality of the results. Our techniques employ simulations to obtain the model\u2019s sensitivity with respect to the initial state (or model\u2019s Lipschitz constant) which is then used to compute reachable states of the system. The approaches also provide probabilistic guarantees on the accuracy of the computed reachable sets that are based on simulations. Each technique requires different levels of information about the black-box system, allowing the readers to select the best technique according to the capabilities of the models. The validation experiments have demonstrated that our proposed algorithms compute accurate reachable sets of stable and unstable linear systems. The approach based on dynamic sensitivity provides an accurate and, with respect to system dimensions, more scalable approach, while the sampling-based method allows a flexible trade-off between accuracy and runtime cost. The validation results also show that our approaches are promising even when applied to nonlinear systems, especially, when applied to larger and more complex systems. The reproducibility package with code and data can be found at\n                    <jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" ext-link-type=\"uri\" xlink:href=\"https:\/\/github.com\/twright\/FMI-Reachability-Reproducibility\">https:\/\/github.com\/twright\/FMI-Reachability-Reproducibility<\/jats:ext-link>\n                    .\n                  <\/jats:p>","DOI":"10.1177\/00375497241261409","type":"journal-article","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T06:26:01Z","timestamp":1721888761000},"page":"575-596","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":2,"title":["Reachability analysis of FMI models using data-driven dynamic sensitivity"],"prefix":"10.1177","volume":"101","author":[{"given":"Sergiy","family":"Bogomolov","sequence":"first","affiliation":[{"name":"School of Computing, Newcastle University, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2692-9742","authenticated-orcid":false,"given":"Cl\u00e1udio","family":"Gomes","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlos","family":"Isasa","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sadegh","family":"Soudjani","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1785-4021","authenticated-orcid":false,"given":"Paulius","family":"Stankaitis","sequence":"additional","affiliation":[{"name":"Department of Computing Science and Mathematics, University of Stirling, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Wright","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2024,7,25]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2018.2873186"},{"key":"e_1_3_3_3_2","volume-title":"Proceedings of the 2021 annual modeling and simulation conference (ANNSIM)","author":"Feng H","unstructured":"Feng H, Gomes C, Thule C, et al. Introduction to digital twin engineering. In: Proceedings of the 2021 annual modeling and simulation conference (ANNSIM), Fairfax, VA, 19\u201322 July 2021. New York: IEEE."},{"key":"e_1_3_3_4_2","volume-title":"Proceedings of the 2022 annual modeling and simulation conference (ANNSIM)","author":"Feng H","unstructured":"Feng H, Gomes C, Gil S, et al. Integration of the Mape-K loop in digital twins. In: Proceedings of the 2022 annual modeling and simulation conference (ANNSIM), San Diego, CA, 18\u201320 July 2022. New York: IEEE."},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1146\/annurev-control-071420-081941"},{"key":"e_1_3_3_6_2","first-page":"89","volume-title":"Proceedings of the leveraging applications of formal methods, verification and validation practice: 11th international symposium (ISoLA 2022; Part IV)","author":"Wright T","unstructured":"Wright T, Gomes C, Woodcock J. Formally verified self-adaptation of an incubator digital twin. In: Proceedings of the leveraging applications of formal methods, verification and validation practice: 11th international symposium (ISoLA 2022; Part IV), Rhodes, 22\u201330 October 2022, pp. 89\u2013109. Berlin; Heidelberg: Springer-Verlag."},{"key":"e_1_3_3_7_2","volume-title":"Linkoping electronic conference proceedings","author":"Junghanns A","year":"2021","unstructured":"Junghanns A, Gomes C, Schulze C, et al. The functional mock\u2014up interface 3.0\u2014new features enabling new applications. In: Linkoping electronic conference proceedings, 20\u201324 September 2021. Link\u00f6ping: Link\u00f6ping University Electronic Press."},{"key":"e_1_3_3_8_2","first-page":"139","volume-title":"Proceedings of the international symposium on leveraging applications of formal methods (ISOLA)","author":"Bogomolov S","unstructured":"Bogomolov S, Fitzgerald J, Soudjani S, et al. Data-driven reachability analysis of digital twin FMI models. In: Proceedings of the international symposium on leveraging applications of formal methods (ISOLA), Rhodes, 22\u201330 October 2022, pp. 139\u2013158. Berlin; Heidelberg: Springer-Verlag."},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"e_1_3_3_11_2","first-page":"39","volume-title":"Proceedings of the 22nd ACM international conference on hybrid systems: computation and control (HSCC\u201919)","author":"Bogomolov S","unstructured":"Bogomolov S, Forets M, Frehse G, et al. JuliaReach: a toolbox for set-based reachability. In: Proceedings of the 22nd ACM international conference on hybrid systems: computation and control (HSCC\u201919), Montreal, QC, Canada, 16\u201318 April 2019, pp. 39\u201344. New York: Association for Computing Machinery (ACM)."},{"key":"e_1_3_3_12_2","first-page":"3","volume-title":"Proceedings of the 11th international Haifa verification conference (HVC 2015; LNCS, Volume 9434)","author":"Ray R","unstructured":"Ray R, Gurung A, Das B, et al. XSpeed: accelerating reachability analysis on multi-core processors. In: Proceedings of the 11th international Haifa verification conference (HVC 2015; LNCS, Volume 9434), Haifa, 17\u201319 November 2015, pp. 3\u201318. Berlin; Heidelberg: Springer."},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2024.101467"},{"key":"e_1_3_3_14_2","first-page":"141","article-title":"Neural abstraction-based controller synthesis and deployment","volume":"22","author":"Majumdar R","year":"2023","unstructured":"Majumdar R, Salamati M, Soudjani S. Neural abstraction-based controller synthesis and deployment. ACM T Embed Comput S 2023; 22: 141.","journal-title":"ACM T Embed Comput S"},{"key":"e_1_3_3_15_2","first-page":"81","volume-title":"Proceedings of the international conference on tools and algorithms for the construction and analysis of systems","author":"Banerjee T","unstructured":"Banerjee T, Majumdar R, Mallik K, et al. A direct symbolic algorithm for solving stochastic Rabin games. In: Proceedings of the international conference on tools and algorithms for the construction and analysis of systems, Munich, 2\u20137 April 2022, pp. 81\u201398. Berlin; Heidelberg: Springer."},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2023.101430"},{"key":"e_1_3_3_17_2","first-page":"174","volume-title":"Proceedings of the 10th international conference on hybrid systems: computation and control (HSCC\u201907)","author":"Donz\u00e9 A","unstructured":"Donz\u00e9 A, Maler O. Systematic simulation using sensitivity analysis. In: Proceedings of the 10th international conference on hybrid systems: computation and control (HSCC\u201907), Pisa, 3\u20135 April 2007, pp. 174\u2013189. Berlin; Heidelberg: Springer."},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/81.828574"},{"key":"e_1_3_3_19_2","first-page":"1","volume-title":"Proceedings of the 2018 IEEE international symposium on circuits and systems (ISCAS)","author":"Geng S","unstructured":"Geng S, Hiskens IA. Jump conditions for second-order trajectory sensitivities at events. In: Proceedings of the 2018 IEEE international symposium on circuits and systems (ISCAS), Florence, 27\u201330 May 2018, pp. 1\u20135. New York: IEEE."},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"e_1_3_3_21_2","first-page":"1","volume-title":"Proceedings of the 2013 11th ACM international conference on embedded software (EMSOFT)","author":"Duggirala PS","unstructured":"Duggirala PS, Mitra S, Viswanathan M. Verification of annotated models from executions. In: Proceedings of the 2013 11th ACM international conference on embedded software (EMSOFT), Montreal, QC, Canada, 29 September\u20134 October 2013, pp. 1\u201310. New York: IEEE."},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_5"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-13050-3_5"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_22"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2015.11.147"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1049\/iet-cps.2018.5017"},{"key":"e_1_3_3_27_2","first-page":"684","volume-title":"Proceedings of the 44th IEEE conference on decision and control","author":"Girard A","unstructured":"Girard A, Pappas GJ. Approximate bisimulations for nonlinear dynamical systems. In: Proceedings of the 44th IEEE conference on decision and control, Seville, 15 December 2005, pp. 684\u2013689. New York: IEEE."},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36580-X_22"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2020.3012251"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2023.3257167"},{"key":"e_1_3_3_31_2","first-page":"2055","volume-title":"Proceedings of the 2020 conference on robot learning: proceedings of machine learning research (PMLR)","author":"Lew T","year":"2020","unstructured":"Lew T, Pavone M. Sampling-based reachability analysis: a random set theory approach with adversarial sampling. In: Kober J, Ramos F, Tomlin C (eds) Proceedings of the 2020 conference on robot learning: proceedings of machine learning research (PMLR), vol. 155. Berlin; Heidelberg: Springer, 2020, pp. 2055\u20132070."},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_17"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-020-00858-7"},{"key":"e_1_3_3_34_2","first-page":"49","article-title":"Co-simulation: a survey","volume":"51","author":"Gomes C","year":"2018","unstructured":"Gomes C, Thule C, Broman D, et al. Co-simulation: a survey. ACM Comput Surv 2018; 51: 49.","journal-title":"ACM Comput Surv"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68111-3_144"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1177\/00375497221097128"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48983-5_10"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54118-6"},{"key":"e_1_3_3_39_2","first-page":"105","volume-title":"Proceedings of the 8th international Modelica conference","author":"Blochwitz T","unstructured":"Blochwitz T, Otter M, Arnold M, et al. The functional mockup interface for tool independent exchange of simulation models. In: Proceedings of the 8th international Modelica conference, Dresden, 20\u201322 March 2011. Link\u00f6ping University Press, pp. 105\u2013114."},{"key":"e_1_3_3_40_2","volume-title":"Simulink user\u2019s guide","author":"The MathWorks","year":"2021","unstructured":"The MathWorks. Simulink user\u2019s guide. Natick, MA: The MathWorks, 2021."},{"key":"e_1_3_3_41_2","first-page":"1588","volume-title":"Proceedings of the 2006 IEEE conference on computer aided control system design","author":"Fritzson P","unstructured":"Fritzson P, Aronsson P, Pop A, et al. OpenModelica\u2014a free open-source environment for system modeling, simulation, and teaching. In: Proceedings of the 2006 IEEE conference on computer aided control system design, Munich, 4\u20136 October 2006, pp. 1588\u20131595. New York: IEEE."},{"key":"e_1_3_3_42_2","first-page":"1","volume-title":"Proceedings of the 2nd international workshop on modelling, analysis, and control of complex CPS (CPS Data)","author":"Larsen PG","unstructured":"Larsen PG, Fitzgerald J, Woodcock J, et al. Integrated tool chain for model-based design of Cyber-Physical Systems: the INTO-CPS project. In: Proceedings of the 2nd international workshop on modelling, analysis, and control of complex CPS (CPS Data), Vienna, 11 April 2016, pp. 1\u20136. New York: IEEE."},{"key":"e_1_3_3_43_2","unstructured":"Robinson RC. Scalar ordinary differential equations. Technical report 2013 https:\/\/sites.math.northwestern.edu\/\u223cclark\/dyn-sys\/scalar.pdf"},{"key":"e_1_3_3_44_2","volume-title":"Randomized algorithms for analysis and control of uncertain systems: with applications","author":"Tempo R","year":"2012","unstructured":"Tempo R, Calafiore G, Dabbene F. Randomized algorithms for analysis and control of uncertain systems: with applications. London: Springer Science+Business Media, 2012."},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2014.2330702"},{"key":"e_1_3_3_46_2","volume-title":"Proceedings of the international conference on learning representations","author":"Weng TW","unstructured":"Weng TW, Zhang H, Chen PY, et al. Evaluating the robustness of neural networks: an extreme value theory approach. In: Proceedings of the international conference on learning representations, Vancouver, BC, Canada, 30 April\u20133 May 2018."},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00229304"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/0-387-34471-3"},{"key":"e_1_3_3_49_2","first-page":"44","volume":"90","author":"Frehse G","year":"2022","unstructured":"Frehse G, Althoff M, Schoitsch E, et al. (eds). Proceedings of the 9th international workshop on applied verification of continuous and hybrid systems (ARCH22). EasyChair, 2022 (also published in Epic Ser Comput2022; 90: 44\u201357). https:\/\/easychair.org\/publications\/paper\/b6cN","journal-title":"Proceedings of the 9th international workshop on applied verification of continuous and hybrid systems (ARCH22)"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41592-019-0686-2"},{"key":"e_1_3_3_51_2","unstructured":"Hindmarsh AC. ODEPACK a systemized collection of ODE solvers 1992 https:\/\/www.osti.gov\/biblio\/145724"},{"key":"e_1_3_3_52_2","first-page":"83","article-title":"CVXPY: a Python-embedded modeling language for convex optimization","volume":"17","author":"Diamond S","year":"2016","unstructured":"Diamond S, Boyd S. CVXPY: a Python-embedded modeling language for convex optimization. J Mach Learn Res 2016; 17: 83.","journal-title":"J Mach Learn Res"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1080\/23307706.2017.1397554"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1016\/0169-2070(92)90008-W"},{"key":"e_1_3_3_55_2","first-page":"339","volume-title":"Runtime verification: 20th international conference, RV 2020","author":"Wright T","year":"2020","unstructured":"Wright T, Stark I. Property-directed verified monitoring of signal temporal logic. In: Deshmukh J, Nickovic D (eds) Runtime verification: 20th international conference, RV 2020, Los Angeles, CA, October 6\u20139, 2020. Berlin; Heidelberg: Springer-Verlag, 2020, pp. 339\u2013358."},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.1177\/00375497231205035"}],"container-title":["SIMULATION"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/00375497241261409","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.1177\/00375497241261409","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/00375497241261409","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T11:34:16Z","timestamp":1777635256000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.1177\/00375497241261409"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,25]]},"references-count":55,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2025,5]]}},"alternative-id":["10.1177\/00375497241261409"],"URL":"https:\/\/doi.org\/10.1177\/00375497241261409","relation":{},"ISSN":["0037-5497","1741-3133"],"issn-type":[{"value":"0037-5497","type":"print"},{"value":"1741-3133","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,7,25]]}}}