{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T19:03:53Z","timestamp":1782846233585,"version":"3.54.5"},"reference-count":0,"publisher":"ECMS","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026,6,23]]},"abstract":"<jats:p>One of the cornerstones in formal system verification is Model Checking (MC), a technique to verify systems against properties expressed in some temporal logic by exhaustive exploration of the state space. While MC can succesfully cope with many cases of practical interests, its ability to scale to systems of substantial size remains an open challenge. Statistical MC (SMC) has been proposed to improve the scalability of MC by confining the exploration to sample traces obtained by executing the system model, and thus yielding estimates of the probability of satisfying given properties instead of Boolean results. Most SMC tools still rely on formal and abstract system models, but such models often miss important details which may hinder the effectiveness of verification. In this paper, we introduce a framework to combine SMC with simulation or even actual execution of some system components. We do this using SMC plugins, i.e., executable components that can be referenced in an extended version of the JANI format, a widely adopted language to specify models for SMC. The plugins can be loaded by a SMC tool during verification and provide feedback about the actual execution of the system which is more accurate than abstract models. We illustrate the feasibility of this technique through two robotics use cases, showing how SMC plugins can be used to effectively model and verify systems<\/jats:p>","DOI":"10.7148\/2026-0629","type":"proceedings-article","created":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T18:08:43Z","timestamp":1782842923000},"page":"629-637","source":"Crossref","is-referenced-by-count":0,"title":["Integrating simulation and verification to assess safety of robot control software"],"prefix":"10.7148","author":[{"given":"Marco","family":"Lampacrescia","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matteo","family":"Palmas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Enrico","family":"Ghiorzi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christian","family":"Henkel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michaela","family":"Klauck","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"4144","published-online":{"date-parts":[[2026,6,23]]},"event":{"name":"40th ECMS International Conference on Modelling and Simulation"},"container-title":["ECMS 2026 Proceedings edited by Filippo Sanfilippo, Florenc Demrozi, Fabio Sgarbossa, Mohammad Poursina"],"original-title":[],"deposited":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T18:08:44Z","timestamp":1782842924000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.scs-europe.net\/dlib\/2026\/ecms2026acceptedpapers\/0629_dis_ecms2026_0023.pdf"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,23]]},"references-count":0,"URL":"https:\/\/doi.org\/10.7148\/2026-0629","relation":{},"subject":[],"published":{"date-parts":[[2026,6,23]]}}}