{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:01:28Z","timestamp":1750309288364,"version":"3.41.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T00:00:00Z","timestamp":1720569600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ANR BisoUS","award":["ANR-22-CE48-0012"],"award-info":[{"award-number":["ANR-22-CE48-0012"]}]},{"name":"VERHYDYN","award":["INS2I-CNRS"],"award-info":[{"award-number":["INS2I-CNRS"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Model. Comput. Simul."],"published-print":{"date-parts":[[2024,7,31]]},"abstract":"<jats:p>We propose a simulation-based technique for the parameterization and the stability analysis of parametric Ordinary Differential Equations. This technique is an adaptation of Statistical Model Checking, often used to verify the validity of biological models, to the setting of Ordinary Differential Equations systems. The aim of our technique is to estimate the probability of satisfying a given property under the variability of the parameter or initial condition of the ODE, with any metrics of choice. To do so, we discretize the values space and use statistical model checking to evaluate each individual value w.r.t. provided data. Contrary to other existing methods, we provide statistical guarantees regarding our results that take into account the unavoidable approximation errors introduced through the numerical integration of the ODE system performed while simulating. In order to show the potential of our technique, we present its application to two case studies taken from the literature, one relative to the growth of a jellyfish population, and the other concerning a well-known oscillator model.<\/jats:p>","DOI":"10.1145\/3649438","type":"journal-article","created":{"date-parts":[[2024,2,24]],"date-time":"2024-02-24T09:17:41Z","timestamp":1708766261000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["End-to-End Statistical Model Checking for Parameterization and Stability Analysis of ODE Models"],"prefix":"10.1145","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1592-8042","authenticated-orcid":false,"given":"David","family":"Julien","sequence":"first","affiliation":[{"name":"Nantes Universit\u00e9, \u00c9cole Centrale Nantes, CNRS, LS2N, UMR 6004, Nantes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-1469-4284","authenticated-orcid":false,"given":"Gilles","family":"Ardourel","sequence":"additional","affiliation":[{"name":"Nantes Universit\u00e9, \u00c9cole Centrale Nantes, CNRS, LS2N, UMR 6004, Nantes France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5122-1194","authenticated-orcid":false,"given":"Guillaume","family":"Cantin","sequence":"additional","affiliation":[{"name":"Nantes Universit\u00e9, \u00c9cole Centrale Nantes, CNRS, LS2N, UMR 6004, Nantes France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9104-4361","authenticated-orcid":false,"given":"Beno\u00eet","family":"Delahaye","sequence":"additional","affiliation":[{"name":"Nantes Universit\u00e9, \u00c9cole Centrale Nantes, CNRS, LS2N, UMR 6004, Nantes France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,7,10]]},"reference":[{"key":"e_1_3_3_2_2","first-page":"79","volume-title":"Proceedings of the Reliable Computing","author":"Sandretto Julien Alexandre dit","year":"2016","unstructured":"Julien Alexandre dit Sandretto and Alexandre Chapoutot. 2016. Validated explicit and implicit runge\u2013kutta methods. In Proceedings of the Reliable Computing. 79\u2013103."},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","unstructured":"Julien Alexandre dit Sandretto and Jian Wan. 2018. Reachability analysis of nonlinear ODEs using polytopic based validated runge\u2013kutta. In Reachability Problems (Lecture Notes in Computer Science Vol. 11123). Springer Cham Switzerland 1\u201314. 10.1007\/978-3-030-00250-3_1","DOI":"10.1007\/978-3-030-00250-3_1"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-21759-4_4"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1086\/260062"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","unstructured":"Olivier Bouissou and Matthieu Martel. 2006. GRKLib: A guaranteed runge\u2013kutta library. In 12th GAMM - IMACS International Symposium on Scientific Computing Computer Arithmetic and Validated Numerics (SCAN\u201906) 8. 10.1109\/SCAN.2006.20","DOI":"10.1109\/SCAN.2006.20"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1002\/9781119121534"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1177\/1748006XJRR312"},{"key":"e_1_3_3_10_2","volume-title":"Analyse num\u00e9rique des \u00e9quations diff\u00e9rentielles","author":"Crouzeix Michel","year":"1984","unstructured":"Michel Crouzeix and Alain L. Mignot. 1984. Analyse num\u00e9rique des \u00e9quations diff\u00e9rentielles. Vol. 1. Masson."},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31862-0_21"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_13"},{"key":"e_1_3_3_13_2","volume-title":"Analyse num\u00e9rique et \u00e9quations diff\u00e9rentielles","author":"Demailly Jean-Pierre","year":"2012","unstructured":"Jean-Pierre Demailly. 2012. Analyse num\u00e9rique et \u00e9quations diff\u00e9rentielles. EDP Sciences."},{"key":"e_1_3_3_14_2","volume-title":"Erzwungene Schwingungen bei ver\u00e4nderlicher Eigenfrequenz und ihre technische Bedeutung","author":"Duffing Georg","year":"1918","unstructured":"Georg Duffing and Fritz Emde. 1918. Erzwungene Schwingungen bei ver\u00e4nderlicher Eigenfrequenz und ihre technische Bedeutung. Vieweg."},{"key":"e_1_3_3_15_2","volume-title":"Linear Operators. 1. General Theory","author":"Dunford Nelson","year":"1967","unstructured":"Nelson Dunford and Jacob Theodore Schwartz. 1967. Linear Operators. 1. General Theory. Interscience Publishers."},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0329-y"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_18"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26916-0_6"},{"key":"e_1_3_3_19_2","volume-title":"Ordinary Differential Equations","author":"Hale Jack K.","year":"1980","unstructured":"Jack K. Hale. 1980. Ordinary Differential Equations. R. E. Krieger Publishing Company."},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2008.19"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1515\/9781400852871"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1963.10500830"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-7462(80)90031-1"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-16336-4_5"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934574"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16612-9_11"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1812.01091"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0025-5718-1951-0043566-3"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1080\/00207179208934253"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7040386"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ecolmodel.2014.07.009"},{"key":"e_1_3_3_33_2","volume-title":"Dynamics and Evolution of Galactic Nuclei","author":"Merritt David","year":"2013","unstructured":"David Merritt. 2013. Dynamics and Evolution of Galactic Nuclei. Princeton University Press, Princeton, NJ, USA. Retrieved from https:\/\/press.princeton.edu\/books\/hardcover\/9780691121017\/dynamics-and-evolution-of-galactic-nuclei"},{"key":"e_1_3_3_34_2","volume-title":"Nonlinear Oscillations","author":"Minorsky Nicholai","year":"1962","unstructured":"Nicholai Minorsky. 1962. Nonlinear Oscillations. Van Nostrand. 62002555"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","unstructured":"N. S. Nedialkov. 2006. Interval tools for ODEs and DAEs. In 12th GAMM - IMACS International Symposium on Scientific Computing Computer Arithmetic and Validated Numerics (SCAN\u201906) 4. 10.1109\/SCAN.2006.28","DOI":"10.1109\/SCAN.2006.28"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0003-8"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1515\/9783112573006"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_38"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_20"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41598-020-62357-5"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1111\/j.1467-9868.2007.00610.x"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","unstructured":"Fedor Shmarov and Paolo Zuliani. 2016. Probabilistic hybrid systems verification via SMT and monte\u2013carlo techniques. In Hardware and Software: Verification and Testing (Lecture Notes in Computer Science Vol. 10028). Springer Cham Switzerland 152\u2013168. 10.1007\/978-3-319-49052-6_10","DOI":"10.1007\/978-3-319-49052-6_10"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1515\/9781400848737"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","unstructured":"Qinsi Wang Paolo Zuliani Soonho Kong Sicun Gao and Edmund M. Clarke. 2015. SReach: A probabilistic bounded delta-reachability analyzer for stochastic hybrid systems. In Computational Methods in Systems Biology (Lecture Notes in Computer Science Vol. 9308). Springer Cham Switzerland 15\u201327. 10.1007\/978-3-319-23401-4_3","DOI":"10.1007\/978-3-319-23401-4_3"},{"key":"e_1_3_3_45_2","volume-title":"Vibration Problems in Engineering, 5th Edition","author":"Jr. W. Weaver,","year":"1991","unstructured":"W. Weaver, Jr., S. P. Timoshenko, and D. H. Young. 1991. Vibration Problems in Engineering, 5th Edition. Wiley, Hoboken, NJ, USA. Retrieved from https:\/\/www.wiley.com\/en-us\/Vibration+Problems+in+Engineering%2C+5th+Edition-p-9780471632283"}],"container-title":["ACM Transactions on Modeling and Computer Simulation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649438","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649438","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:03:21Z","timestamp":1750291401000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649438"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,10]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,7,31]]}},"alternative-id":["10.1145\/3649438"],"URL":"https:\/\/doi.org\/10.1145\/3649438","relation":{},"ISSN":["1049-3301","1558-1195"],"issn-type":[{"type":"print","value":"1049-3301"},{"type":"electronic","value":"1558-1195"}],"subject":[],"published":{"date-parts":[[2024,7,10]]},"assertion":[{"value":"2023-03-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-02-04","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-07-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}