{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,23]],"date-time":"2025-10-23T17:04:37Z","timestamp":1761239077173,"version":"3.37.3"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2023,4,14]],"date-time":"2023-04-14T00:00:00Z","timestamp":1681430400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,4,14]],"date-time":"2023-04-14T00:00:00Z","timestamp":1681430400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"name":"Horizon 2020 Research and Innovation","award":["730080"],"award-info":[{"award-number":["730080"]}]},{"name":"Horizon 2020 Research and Innovation","award":["700665"],"award-info":[{"award-number":["700665"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2024,3]]},"DOI":"10.1007\/s11334-023-00527-0","type":"journal-article","created":{"date-parts":[[2023,4,17]],"date-time":"2023-04-17T08:02:32Z","timestamp":1681718552000},"page":"3-16","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Model-based design of resilient systems using quantitative risk assessment"],"prefix":"10.1007","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4256-0383","authenticated-orcid":false,"given":"Braham Lotfi","family":"Mediouni","sequence":"first","affiliation":[]},{"given":"Iulia","family":"Dragomir","sequence":"additional","affiliation":[]},{"given":"Ayoub","family":"Nouri","sequence":"additional","affiliation":[]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,14]]},"reference":[{"issue":"12","key":"527_CR1","doi-asserted-by":"publisher","first-page":"1563","DOI":"10.1016\/j.robot.2012.09.005","volume":"60","author":"T Abdellatif","year":"2012","unstructured":"Abdellatif T, Bensalem S, Combaz J et al (2012) Rigorous design of robot software: a formal component-based approach. Robot Autonom Syst 60(12):1563\u20131578. https:\/\/doi.org\/10.1016\/j.robot.2012.09.005","journal-title":"Robot Autonom Syst"},{"issue":"2","key":"527_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183\u2013235","journal-title":"Theor Comput Sci"},{"issue":"1","key":"527_CR3","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur R, Henzinger T (1993) Real-time logics: complexity and expressiveness. Inf Comput 104(1):35\u201377. https:\/\/doi.org\/10.1006\/inco.1993.1025","journal-title":"Inf Comput"},{"key":"527_CR4","unstructured":"Baier C, Katoen JP (2008) Principles of model checking (representation and mind series). The MIT Press"},{"key":"527_CR5","doi-asserted-by":"crossref","unstructured":"Basu A, Bensalem S, Bozga M et al (2010) Statistical abstraction and model-checking of large heterogeneous systems. Forum for fundamental research on theory, FORTE\u201910, LNCS, vol 6117. Springer, Berlin Heidelberg, Berlin, Heidelberg, pp 32\u201346","DOI":"10.1007\/978-3-642-13464-7_4"},{"key":"527_CR6","doi-asserted-by":"crossref","unstructured":"Basu A, Bensalem S, Bozga M, et\u00a0al (2010b) Verification of an AFDX Infrastructure using Simulations and Probabilities. In: Runtime Verification, RV\u201910, LNCS, vol 6418. Springer Berlin Heidelberg","DOI":"10.1007\/978-3-642-16612-9_25"},{"key":"527_CR7","doi-asserted-by":"publisher","unstructured":"Batteux M, Prosvirnova T, Rauzy A, et\u00a0al (2013) The AltaRica 3.0 project for model-based safety assessment. In: 11th IEEE international conference on industrial informatics, INDIN 2013, Bochum, Germany, July 29-31, 2013. IEEE, pp 741\u2013746, https:\/\/doi.org\/10.1109\/INDIN.2013.6622976","DOI":"10.1109\/INDIN.2013.6622976"},{"key":"527_CR8","doi-asserted-by":"publisher","unstructured":"Bensalem S, de\u00a0Silva L, Griesmayer A, et\u00a0al (2011) A formal approach for incremental construction with an application to autonomous robotic systems. In: Apel S, Jackson EK (eds) Software composition: 10th international conference, SC 2011, Zurich, Switzerland, June 30 - July 1, 2011. Proceedings, Lecture Notes in Computer Science, vol 6708. Springer, pp 116\u2013132, https:\/\/doi.org\/10.1007\/978-3-642-22045-6_8","DOI":"10.1007\/978-3-642-22045-6_8"},{"key":"527_CR9","first-page":"82","volume":"2014","author":"B Bittner","year":"2014","unstructured":"Bittner B, Bozzano M, Cimatti A et al (2014) An integrated process for FDIR design in aerospace. IMBSA 2014:82\u201395","journal-title":"IMBSA"},{"key":"527_CR10","first-page":"533","volume":"2016","author":"B Bittner","year":"2016","unstructured":"Bittner B, Bozzano M, Cavada R et al (2016) The xSAP safety analysis platform. TACAS 2016:533\u2013539","journal-title":"TACAS"},{"key":"527_CR11","doi-asserted-by":"crossref","unstructured":"Bornot S, Sifakis J, Tripakis S (1997) Modeling urgency in timed systems. In: International symposium on compositionality, Springer, pp 103\u2013129","DOI":"10.1007\/3-540-49213-5_5"},{"key":"527_CR12","doi-asserted-by":"crossref","unstructured":"Cavada R, Cimatti A, Dorigatti M, et\u00a0al (2014) The nuxmv symbolic model checker. In: International conference on computer aided verification. Springer, pp 334\u2013342","DOI":"10.1007\/978-3-319-08867-9_22"},{"issue":"3","key":"527_CR13","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/s10009-014-0323-4","volume":"17","author":"A David","year":"2015","unstructured":"David A, Larsen K, Legay A et al (2015) Statistical model checking for biological systems. Int J Softw Tools Technol Transf (STTT) 17(3):351\u2013367","journal-title":"Int J Softw Tools Technol Transf (STTT)"},{"issue":"4","key":"527_CR14","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David A, Larsen KG, Legay A et al (2015) Uppaal SMC tutorial. STTT 17(4):397\u2013415","journal-title":"STTT"},{"key":"527_CR15","doi-asserted-by":"crossref","unstructured":"Desai A, Qadeer S, Seshia SA (2018) Programming safe robotics systems: challenges and advances. In: International symposium on leveraging applications of formal methods. Springer, pp 103\u2013119","DOI":"10.1007\/978-3-030-03421-4_8"},{"key":"527_CR16","unstructured":"Dragomir I (2019) ESROCOS planetary exploration demonstrator: the watchdog component in TASTE and BIP. https:\/\/github.com\/ESROCOS\/control-mc_watchdog"},{"key":"527_CR17","doi-asserted-by":"crossref","unstructured":"Dragomir I, Iosti S, Bozga M et al (2018) Designing systems with detection and reconfiguration capabilities: a formal approach. In: Steffen B, Margaria T (eds) Leveraging applications of formal methods, verification and validation: 8th international symposium, ISoLA 2018, Lymassol, Cyprus, November 5\u20139, 2018. Springer, Lecture Notes in Computer Science","DOI":"10.1007\/978-3-030-03424-5_11"},{"key":"527_CR18","unstructured":"ESROCOS (2019a) ESROCOS Planetary Exploration Demonstrator. https:\/\/github.com\/ESROCOS\/plex-demonstrator-record"},{"key":"527_CR19","unstructured":"ESROCOS (2019b) ESROCOS Project Github Repository. https:\/\/github.com\/ESROCOS"},{"key":"527_CR20","doi-asserted-by":"crossref","unstructured":"Foughali M, Berthomieu B, Dal\u00a0Zilio S, et\u00a0al (2018) Formal verification of complex robotic systems on resource-constrained platforms. In: FormaliSE: 6th international conference on formal methods in software engineering","DOI":"10.1145\/3193992.3193996"},{"key":"527_CR21","doi-asserted-by":"crossref","unstructured":"H\u00e9rault T, Lassaigne R, Magniette F, et\u00a0al (2004) Approximate probabilistic model checking. In: International conference on verification, model checking, and abstract interpretation, VMCAI\u201904, pp 73\u201384","DOI":"10.1007\/978-3-540-24622-0_8"},{"key":"527_CR22","doi-asserted-by":"crossref","unstructured":"Jegourel C, Legay A, Sedwards S (2013) Importance splitting for statistical model checking rare properties. In: CAV. Springer, pp 576\u2013591","DOI":"10.1007\/978-3-642-39799-8_38"},{"issue":"5","key":"527_CR23","first-page":"263","volume":"1","author":"H Kahn","year":"1953","unstructured":"Kahn H, Marshall AW (1953) Methods of reducing sample size in Monte Carlo computations. J Oper Res Soc Am 1(5):263\u2013278","journal-title":"J Oper Res Soc Am"},{"key":"527_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-1772-0","volume-title":"Introduction to modeling and analysis of stochastic systems","author":"VG Kulkarni","year":"2011","unstructured":"Kulkarni VG (2011) Introduction to modeling and analysis of stochastic systems. Springer, New York"},{"key":"527_CR25","doi-asserted-by":"crossref","unstructured":"Mediouni BL, Nouri A, Bozga M, et\u00a0al (2018) $${\\cal{S}\\text{BIP}}$$ 2.0: Statistical model checking stochastic real-time systems. In: Lahiri SK, Wang C (eds) Automated technology for verification and analysis: 16th international symposium, ATVA, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, LNCS, vol 11138. Springer, pp 536\u2013542","DOI":"10.1007\/978-3-030-01090-4_33"},{"issue":"12","key":"527_CR26","doi-asserted-by":"publisher","first-page":"1312","DOI":"10.1177\/0278364917733549","volume":"36","author":"S Mitsch","year":"2017","unstructured":"Mitsch S, Ghorbal K, Vogelbacher D et al (2017) Formal verification of obstacle avoidance and navigation of ground robots. Int J Robot Res 36(12):1312\u20131340","journal-title":"Int J Robot Res"},{"key":"527_CR27","unstructured":"Munoz M, Montano G, Wirkus M, et\u00a0al (2017) ESROCOS: a robotic operating system for space and terrestrial applications. In: Symposium on advanced space technologies in robotics and automation (ASTRA) 2017, Leiden, Netherlands, June 20-22, 2017"},{"issue":"3\u20134","key":"527_CR28","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1504\/IJCCBS.2018.096439","volume":"8","author":"A Nouri","year":"2018","unstructured":"Nouri A, Mediouni BL, Bozga M et al (2018) Performance evaluation of stochastic real-time systems with the SBIP framework. Int J Crit Comput-Based Syst 8(3\u20134):340\u2013370. https:\/\/doi.org\/10.1504\/IJCCBS.2018.096439","journal-title":"Int J Crit Comput-Based Syst"},{"key":"527_CR29","unstructured":"Ocon J, Colemenero F, Estremera J, et\u00a0al (2018) The ERGO framework and its use in planetary\/orbital scenarios. In: International astronautical congress (IAC) 2018, Bremen, Germany, October 1-5, 2018"},{"key":"527_CR30","doi-asserted-by":"publisher","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, Providence, Rhode Island, USA, 31 October\u20131 November 1977, pp 46\u201357, https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"527_CR31","doi-asserted-by":"crossref","unstructured":"Raman B, Nouri A, Gangadharan D, et\u00a0al (2013) Stochastic modeling and performance analysis of multimedia SoCs. In: International conference on systems, architectures, modeling and simulation, SAMOS\u201913, pp 145\u2013154","DOI":"10.1109\/SAMOS.2013.6621117"},{"key":"527_CR32","doi-asserted-by":"crossref","unstructured":"Tosun T, Jing G, Kress-Gazit H, et\u00a0al (2018) Computer-aided compositional design and verification for modular robots. In: Robotics research. Springer, pp 237\u2013252","DOI":"10.1007\/978-3-319-51532-8_15"},{"key":"527_CR33","unstructured":"Wander A, Forstner R (2012) Innovative Fault Detection. State of the Art and Research Challenges. Deutscher Luft- und Raumfahrtkongress, Isolation and Recovery Strategies On-board Spacecraft"},{"key":"527_CR34","unstructured":"Younes HLS (2005) Verification and planning for stochastic processes with asynchronous events. PhD thesis, Carnegie Mellon"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-023-00527-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-023-00527-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-023-00527-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,20]],"date-time":"2024-02-20T10:20:35Z","timestamp":1708424435000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-023-00527-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,14]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,3]]}},"alternative-id":["527"],"URL":"https:\/\/doi.org\/10.1007\/s11334-023-00527-0","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"type":"print","value":"1614-5046"},{"type":"electronic","value":"1614-5054"}],"subject":[],"published":{"date-parts":[[2023,4,14]]},"assertion":[{"value":"12 April 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 March 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 April 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The model sources used in this manuscript are available at . The SMC-BIP tool can be downloaded from .","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"The model sources"}}]}}