{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T23:17:33Z","timestamp":1778541453905,"version":"3.51.4"},"reference-count":74,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2023,7,12]],"date-time":"2023-07-12T00:00:00Z","timestamp":1689120000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,7,12]],"date-time":"2023-07-12T00:00:00Z","timestamp":1689120000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"publisher","award":["780089"],"award-info":[{"award-number":["780089"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Supercomput"],"published-print":{"date-parts":[[2024,1]]},"DOI":"10.1007\/s11227-023-05483-x","type":"journal-article","created":{"date-parts":[[2023,7,12]],"date-time":"2023-07-12T08:01:35Z","timestamp":1689148895000},"page":"1206-1237","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Deploying warehouse robots with confidence: the BRAIN-IoT framework\u2019s functional assurance"],"prefix":"10.1007","volume":"80","author":[{"given":"Abdelhakim","family":"Baouya","sequence":"first","affiliation":[]},{"given":"Salim","family":"Chehida","sequence":"additional","affiliation":[]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[]},{"given":"Levent","family":"G\u00fcrgen","sequence":"additional","affiliation":[]},{"given":"Richard","family":"Nicholson","sequence":"additional","affiliation":[]},{"given":"Miquel","family":"Cantero","sequence":"additional","affiliation":[]},{"given":"Mario","family":"Diaznava","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Ferrera","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,12]]},"reference":[{"key":"5483_CR1","unstructured":"International Federation of Robotics (2020) Ifr annual report. https:\/\/ifr.org\/downloads\/press2018\/Presentation_WR_2020.pdf"},{"key":"5483_CR2","doi-asserted-by":"publisher","first-page":"859","DOI":"10.1016\/j.future.2019.05.074","volume":"100","author":"MJM Dourado Carlos","year":"2019","unstructured":"Dourado Carlos MJM et al (2019) A new approach for mobile robot localization based on an online IoT system. Future Gener Comput Syst 100:859\u2013881","journal-title":"Future Gener Comput Syst"},{"key":"5483_CR3","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1016\/j.future.2018.04.081","volume":"86","author":"Z Dingju","year":"2018","unstructured":"Dingju Z (2018) IoT and big data based cooperative logistical delivery scheduling method and cloud robot system. Future Gener Comput Syst 86:709\u2013715. https:\/\/doi.org\/10.1016\/j.future.2018.04.081","journal-title":"Future Gener Comput Syst"},{"key":"5483_CR4","doi-asserted-by":"publisher","DOI":"10.1016\/j.iot.2019.100128","volume":"9","author":"D Coquin","year":"2020","unstructured":"Coquin D, Boukezzoula R, Benoit A, Long NT (2020) Assistance via IoT networking cameras and evidence theory for 3d object instance recognition: application for the nao humanoid robot. Internet Things 9:100128. https:\/\/doi.org\/10.1016\/j.iot.2019.100128","journal-title":"Internet Things"},{"key":"5483_CR5","unstructured":"The Economist (2014) The bots in the warehouse, new robots\u2013smarter and faster\u2013are taking over warehouses. https:\/\/www.economist.com\/science-and-technology\/a-new-generation-of-smarter-and-faster-robots-are-taking-over-distribution-centres\/21807595"},{"key":"5483_CR6","doi-asserted-by":"publisher","unstructured":"Rameez C, Manju C (2021) Orchestration of automated guided mobile robots for transportation task in a warehouse like environment. 5:1\u20137. https:\/\/doi.org\/10.1109\/ETI4.051663.2021.9619354","DOI":"10.1109\/ETI4.051663.2021.9619354"},{"key":"5483_CR7","doi-asserted-by":"publisher","first-page":"103981","DOI":"10.1016\/j.robot.2021.103981","volume":"150","author":"C Mello Ricardo","year":"2022","unstructured":"Mello Ricardo C et al (2022) The poundcloud framework for ROS-based cloud robotics: case studies on autonomous navigation and human-robot interaction. Robot Auton Syst 150:103981. https:\/\/doi.org\/10.1016\/j.robot.2021.103981","journal-title":"Robot Auton Syst"},{"key":"5483_CR8","doi-asserted-by":"publisher","unstructured":"Hiejima T, Kawashima S, Ke M, Kawahara T (2019) Effectiveness of synchronization and cooperative behavior of multiple robots based on swarm AI. In: 2019 IEEE Asia Pacific Conference on Circuits and Systems (APCCAS). pp 341\u2013344. https:\/\/doi.org\/10.1109\/APCCAS47518.2019.8953108","DOI":"10.1109\/APCCAS47518.2019.8953108"},{"key":"5483_CR9","doi-asserted-by":"publisher","first-page":"1687","DOI":"10.1155\/2012\/698046","volume":"698046","author":"A Khamis","year":"2012","unstructured":"Khamis A, ElGindy A (2012) Minefield mapping using cooperative multirobot systems. J Robot 698046:1687. https:\/\/doi.org\/10.1155\/2012\/698046","journal-title":"J Robot"},{"key":"5483_CR10","doi-asserted-by":"publisher","unstructured":"Michael N, Zavlanos MM, Kumar V, Pappas GJ (2008) Distributed multi-robot task assignment and formation control. In: 2008 IEEE International Conference on Robotics and Automation. pp 128\u2013133. https:\/\/doi.org\/10.1109\/ROBOT.2008.4543197","DOI":"10.1109\/ROBOT.2008.4543197"},{"key":"5483_CR11","doi-asserted-by":"publisher","unstructured":"Ji S-H, Han J-S, Lee S-M, Moon Y-S, Kuc T-Y (2011) Collective searching algorithm for multi-robot system with bounded communication range. In: 2011 8th international conference on ubiquitous robots and ambient intelligence (URAI). pp 180\u2013183. https:\/\/doi.org\/10.1109\/URAI.2011.6145956","DOI":"10.1109\/URAI.2011.6145956"},{"issue":"2","key":"5483_CR12","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1109\/TRO.2015.2397771","volume":"31","author":"SG Lee","year":"2015","unstructured":"Lee SG, Diaz-Mercado Y, Egerstedt M (2015) Multirobot control using time-varying density functions. IEEE Trans Robot 31(2):489\u2013493. https:\/\/doi.org\/10.1109\/TRO.2015.2397771","journal-title":"IEEE Trans Robot"},{"key":"5483_CR13","doi-asserted-by":"publisher","unstructured":"Kim K, Park M, Lee S-M, Ji S-H (2012) Development of a dependable network using collective robots with restricted communication range. In: 2012 9th International Conference on Ubiquitous Robots and Ambient Intelligence (URAI). pp 408\u2013412. https:\/\/doi.org\/10.1109\/URAI.2012.6463027","DOI":"10.1109\/URAI.2012.6463027"},{"key":"5483_CR14","doi-asserted-by":"publisher","first-page":"73890","DOI":"10.1109\/ACCESS.2021.3080517","volume":"9","author":"T Papadopoulos Georgios","year":"2021","unstructured":"Papadopoulos Georgios T, Margherita A, Constantine S (2021) Towards open and expandable cognitive ai architectures for large-scale multi-agent human-robot collaborative learning. IEEE Access 9:73890\u201373909. https:\/\/doi.org\/10.1109\/ACCESS.2021.3080517","journal-title":"IEEE Access"},{"key":"5483_CR15","doi-asserted-by":"publisher","first-page":"117900","DOI":"10.1109\/ACCESS.2020.3003991","volume":"8","author":"C Nam","year":"2020","unstructured":"Nam C, Lee S, Lee J, Cheong SH, Kim DH, Kim C, Kim I, Park S-K (2020) A software architecture for service robots manipulating objects in human environments. IEEE Access 8:117900\u2013117920. https:\/\/doi.org\/10.1109\/ACCESS.2020.3003991","journal-title":"IEEE Access"},{"key":"5483_CR16","doi-asserted-by":"publisher","first-page":"102304","DOI":"10.1016\/j.ijinfomgt.2020.102304","volume":"57","author":"D Zhang","year":"2021","unstructured":"Zhang D, Pee LG, Cui L (2021) Artificial intelligence in e-commerce fulfillment: a case study of resource orchestration at Alibaba\u2019s smart warehouse. Int J Inf Manag 57:102304. https:\/\/doi.org\/10.1016\/j.ijinfomgt.2020.102304","journal-title":"Int J Inf Manag"},{"key":"5483_CR17","unstructured":"Systems Robotnik (2020) Robotnik in Brain-IoT. https:\/\/robotnik.eu\/projects\/brain-iot-en"},{"key":"5483_CR18","unstructured":"Armerding T (2020) Security bugs and flaws: both bad, but in different ways. https:\/\/www.synopsys.com\/blogs\/software-security\/security-flaws-vs-bugs"},{"key":"5483_CR19","volume-title":"Building reliable component-based software systems","author":"I Crnkovic","year":"2002","unstructured":"Crnkovic I, Larsson M (2002) Building reliable component-based software systems. Artech House Inc., USA"},{"issue":"5","key":"5483_CR20","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1109\/MS.2003.1231146","volume":"20","author":"B Selic","year":"2003","unstructured":"Selic B (2003) The pragmatics of model-driven development. IEEE Softw 20(5):19\u201325. https:\/\/doi.org\/10.1109\/MS.2003.1231146","journal-title":"IEEE Softw"},{"key":"5483_CR21","doi-asserted-by":"publisher","first-page":"110720","DOI":"10.1016\/j.jss.2020.110720","volume":"169","author":"B Costa","year":"2020","unstructured":"Costa B, Pires PF, Delicato FC (2020) Towards the adoption of omg standards in the development of Soa-based IoT systems. J Syst Softw 169:110720. https:\/\/doi.org\/10.1016\/j.jss.2020.110720","journal-title":"J Syst Softw"},{"key":"5483_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.compind.2018.10.007","volume":"105","author":"B Abdelhakim","year":"2019","unstructured":"Abdelhakim B, Otmane AM, Djamal B, Samir O (2019) Safety analysis of train control system based on model-driven design methodology. Comput Indus 105:1\u201316. https:\/\/doi.org\/10.1016\/j.compind.2018.10.007","journal-title":"Comput Indus"},{"key":"5483_CR23","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-030-71906-7_4","volume-title":"Advances in service-oriented and cloud computing","author":"A Baouya","year":"2021","unstructured":"Baouya A et al (2021) Formal modeling and simulation of collaborative intelligent robots. In: Christian Z et al (eds) Advances in service-oriented and cloud computing. Springer, Cham, pp 41\u201352"},{"key":"5483_CR24","doi-asserted-by":"publisher","unstructured":"Lech J, Radovan S (2021) Proceedings of the 2nd Summer School on Cyber- Physical Systems and Internet-of-Things, vol II. https:\/\/doi.org\/10.5281\/zenodo.5086365","DOI":"10.5281\/zenodo.5086365"},{"issue":"5","key":"5483_CR25","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/s10009-020-00596-7","volume":"23","author":"R El Ballouli","year":"2021","unstructured":"El Ballouli R, Bensalem S, Bozga M, Sifakis J (2021) Programming dynamic reconfigurable systems. Int J Softw Tools Technol Transf 23(5):701\u2013719. https:\/\/doi.org\/10.1007\/s10009-020-00596-7","journal-title":"Int J Softw Tools Technol Transf"},{"key":"5483_CR26","doi-asserted-by":"publisher","unstructured":"Baouya A, Chehida S, et al (2020) A formal modeling and verification of blockchain consensus protocol for IoT systems. In: Hamido F, Ali S (eds) Knowledge innovation through intelligent software methodologies, tools and techniques (SoMeT_20), Kitakyushu, Japan, 20\u201322 September 2020, vol 327 of frontiers in artificial intelligence and applications. IOS Press, pp 330\u2013342. https:\/\/doi.org\/10.3233\/FAIA200578","DOI":"10.3233\/FAIA200578"},{"issue":"8","key":"5483_CR27","doi-asserted-by":"publisher","first-page":"8874","DOI":"10.1007\/s10489-021-02884-4","volume":"52","author":"A Baouya","year":"2022","unstructured":"Baouya A, Chehida S, Ouchani S, Bensalem S, Bozga M (2022) Generation and verification of learned stochastic automata using k-nn and statistical model checking. Appl Intell 52(8):8874\u20138894. https:\/\/doi.org\/10.1007\/s10489-021-02884-4","journal-title":"Appl Intell"},{"key":"5483_CR28","series-title":"Lecture notes in computer science","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1007\/978-3-030-01090-4_33","volume-title":"Automated technology for verification and analysis","author":"BL Mediouni","year":"2018","unstructured":"Mediouni BL et al (2018) Bensalem Saddek S-BIP 2.0: statistical model checking stochastic real-time systems. In: Shuvendu KL, Chao W (eds) Automated technology for verification and analysis. Lecture notes in computer science. Springer, Cham, pp 536\u2013542"},{"key":"5483_CR29","doi-asserted-by":"crossref","unstructured":"Nouri A, Mediouni BL, Bozga M, Combaz J, Bensalem S, Legay A (2018) Performance evaluation of stochastic real-time systems with the SBIP framework. Int J Critic Computer-Based Syst 1\u201333","DOI":"10.1504\/IJCCBS.2018.096439"},{"issue":"1","key":"5483_CR30","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/TRO.2019.2937471","volume":"36","author":"F Vicentini","year":"2020","unstructured":"Vicentini F, Askarpour M, Rossi MG, Mandrioli D (2020) Safety assessment of collaborative robotics through automated formal verification. IEEE Trans Robot 36(1):42\u201361. https:\/\/doi.org\/10.1109\/TRO.2019.2937471","journal-title":"IEEE Trans Robot"},{"issue":"3","key":"5483_CR31","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s10846-021-01386-2","volume":"102","author":"A Mehrnoosh","year":"2021","unstructured":"Mehrnoosh A, Livia L, Samuele L, Niccol\u00f2 I, Matteo R, Federico V (2021) Formally-based model-driven development of collaborative robotic applications. J Intell Robot Syst 102(3):59. https:\/\/doi.org\/10.1007\/s10846-021-01386-2","journal-title":"J Intell Robot Syst"},{"key":"5483_CR32","unstructured":"Zot (2012) A bounded satisfiability checker. http:\/\/github.com\/fm-polimi\/zot"},{"key":"5483_CR33","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/j.ssci.2015.12.017","volume":"84","author":"J Guiochet","year":"2016","unstructured":"Guiochet J (2016) Hazard analysis of human-robot interactions with hazop-uml. Saf Sci 84:225\u2013237. https:\/\/doi.org\/10.1016\/j.ssci.2015.12.017","journal-title":"Saf Sci"},{"issue":"2","key":"5483_CR34","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1109\/THMS.2015.2425139","volume":"46","author":"W Matt","year":"2016","unstructured":"Matt W, Clare D, Michael F, Maha S, Joe S, Lee KK, Kerstin D, Joan S-P (2016) Toward reliable autonomous robotic assistants through formal verification: a case study. IEEE Trans Human-Mach Syst 46(2):186\u2013196. https:\/\/doi.org\/10.1109\/THMS.2015.2425139","journal-title":"IEEE Trans Human-Mach Syst"},{"key":"5483_CR35","unstructured":"Ben-Ari M (2008) Principles of the spin model checker, 1 edn. ISBN 1846287693"},{"key":"5483_CR36","doi-asserted-by":"crossref","unstructured":"Dixon C, et al (2014) \u201cThe fridge door is open\u201d-temporal verification of a robotic assistant\u2019s behaviours. In: TAROS","DOI":"10.1007\/978-3-319-10401-0_9"},{"key":"5483_CR37","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer aided verification","author":"A Cimatti","year":"1999","unstructured":"Cimatti A et al (1999) A new symbolic model verifier. In: Nicolas H, Doron P (eds) Computer aided verification. Springer, Berlin, pp 495\u2013499"},{"key":"5483_CR38","doi-asserted-by":"publisher","unstructured":"Mohammed A, Furbach U, Stolzenburg F (2010) Multi-robot systems: modeling, specification, and model checking. 01. ISBN 978-953-307-036-0. https:\/\/doi.org\/10.5772\/7349","DOI":"10.5772\/7349"},{"key":"5483_CR39","doi-asserted-by":"crossref","unstructured":"Walter D, T\u00e4ubig H, L\u00fcth C (2010) Experiences in applying formal verification in robotics. In: Proceedings of the 29th International Conference on Computer Safety, Reliability, and Security. SAFECOMP\u201910. Springer-Verlag, Berlin, pp 347\u2013360","DOI":"10.1007\/978-3-642-15651-9_26"},{"key":"5483_CR40","doi-asserted-by":"publisher","first-page":"102766","DOI":"10.1016\/j.scico.2021.102766","volume":"216","author":"Y Murray","year":"2022","unstructured":"Murray Y, Sirev\u00e5g M, Ribeiro P, Anisi DA, Mossige M (2022) Safety assurance of an industrial robotic control system using hardware\/software co-verification. Sci Comput Programm 216:102766. https:\/\/doi.org\/10.1016\/j.scico.2021.102766","journal-title":"Sci Comput Programm"},{"issue":"5","key":"5483_CR41","doi-asserted-by":"publisher","first-page":"3097","DOI":"10.1007\/s10270-018-00710-z","volume":"18","author":"A Miyazawa","year":"2019","unstructured":"Miyazawa A, Ribeiro P, Li W et al (2019) Robochart: modelling and verification of the functional behaviour of robotic applications. Softw Syst Model 18(5):3097\u20133149. https:\/\/doi.org\/10.1007\/s10270-018-00710-z","journal-title":"Softw Syst Model"},{"key":"5483_CR42","unstructured":"MathWorks (2021) Simulink design verifier. Accessed 1 Oct from https:\/\/www.mathworks.com\/products\/simulink-design-verifier.html"},{"key":"5483_CR43","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson T, Armstrong P, Boulgakov A, Roscoe AW (2014) Fdr3\u2014a modern refinement checker for csp. In: Erika \u00c1, Klaus H (eds) Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 187\u2013201","DOI":"10.1007\/978-3-642-54862-8_13"},{"issue":"2","key":"5483_CR44","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s00236-020-00394-3","volume":"59","author":"J Baxter","year":"2022","unstructured":"Baxter J, Ribeiro P, Cavalcanti A (2022) Sound reasoning in tock-csp. Acta Inf 59(2):125\u2013162. https:\/\/doi.org\/10.1007\/s00236-020-00394-3","journal-title":"Acta Inf"},{"key":"5483_CR45","doi-asserted-by":"publisher","first-page":"104387","DOI":"10.1016\/j.robot.2023.104387","volume":"163","author":"L Livia","year":"2023","unstructured":"Livia L, Davide Z, Bersani Marcello M, Matteo R (2023) Specification, stochastic modeling and analysis of interactive service robotic applications. Robot Auton Syst. 163:104387. https:\/\/doi.org\/10.1016\/j.robot.2023.104387","journal-title":"Robot Auton Syst."},{"issue":"4","key":"5483_CR46","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, Miku\u010dionis M, Poulsen DB (2015) Uppaal smc tutorial. Int J Softw Tools Technol Trans 17(4):397\u2013415","journal-title":"Int J Softw Tools Technol Trans"},{"key":"5483_CR47","doi-asserted-by":"publisher","unstructured":"Chowdhary RR, Chattopadhyay MK (2021) Orchestration of automated guided mobile robots for transportation task in a warehouse like environment. In: 2021 Emerging trends in industry 4.0 (ETI 4.0), pp 1\u20137. https:\/\/doi.org\/10.1109\/ETI4.051663.2021.9619354","DOI":"10.1109\/ETI4.051663.2021.9619354"},{"key":"5483_CR48","doi-asserted-by":"publisher","unstructured":"Delgado C, Zanzi L, Li X, Costa-P\u00e9rez X (2022) Oros: orchestrating ros-driven collaborative connected robots in mission-critical operations. In: 2022 IEEE 23rd international symposium on a world of wireless, mobile and multimedia networks (WoWMoM), pp 147\u2013156. https:\/\/doi.org\/10.1109\/WoWMoM54355.2022.00026","DOI":"10.1109\/WoWMoM54355.2022.00026"},{"key":"5483_CR49","doi-asserted-by":"publisher","unstructured":"Tahir A, Saghar K, Khalid HB, Shadab\u00a0BU, Khan US, Asad U (2019) Formal verification and development of an autonomous firefighting robotic model. In 2019 International Conference on Robotics and Automation in Industry (ICRAI), pp 1\u20136. https:\/\/doi.org\/10.1109\/ICRAI47710.2019.8967388","DOI":"10.1109\/ICRAI47710.2019.8967388"},{"key":"5483_CR50","doi-asserted-by":"publisher","first-page":"107649","DOI":"10.1016\/j.ress.2021.107649","volume":"213","author":"S Danielle","year":"2021","unstructured":"Danielle S et al (2021) AADL-based safety analysis using formal methods applied to aircraft digital systems. Reliab Eng Syst Saf 213:107649. https:\/\/doi.org\/10.1016\/j.ress.2021.107649","journal-title":"Reliab Eng Syst Saf"},{"key":"5483_CR51","unstructured":"Simonds D (2017) Prism. Prism statistical model checker. http:\/\/www.prismmodelchecker.org\/manual\/RunningPRISM\/StatisticalModelChecking"},{"key":"5483_CR52","doi-asserted-by":"publisher","unstructured":"Baouya A, Mohamed OA, Ouchani S, Bennouar D (2021) Reliability-driven automotive software deployment based on a parametrizable probabilistic model checking. In: Expert Systems with Applications, pp 114572. https:\/\/doi.org\/10.1016\/j.eswa.2021.114572","DOI":"10.1016\/j.eswa.2021.114572"},{"issue":"2","key":"5483_CR53","doi-asserted-by":"publisher","first-page":"2180","DOI":"10.1007\/s11227-022-04741-8","volume":"79","author":"A Baouya","year":"2023","unstructured":"Baouya A, Mohamed OA, Ouchani S (2023) Toward a context-driven deployment optimization for embedded systems: a product line approach. J Supercomput 79(2):2180\u20132211. https:\/\/doi.org\/10.1007\/s11227-022-04741-8","journal-title":"J Supercomput"},{"key":"5483_CR54","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-319-33410-3_21","volume-title":"Modelling and implementation of complex systems","author":"A Baouya","year":"2016","unstructured":"Baouya A et al (2016) A formal approach for maintainability and availability assessment using probabilistic model checking. In: Salim C et al (eds) Modelling and implementation of complex systems. Springer, Cham, pp 295\u2013309"},{"key":"5483_CR55","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D (2011) Prism 4.0: verification of probabilistic real-time systems. In: Ganesh G, Shaz Q (eds) Computer Aided Verification, vol 6806. Lecture Notes in Computer Science. Springer Berlin Heidelberg, pp 585\u2013591","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"5483_CR56","doi-asserted-by":"publisher","unstructured":"Chehida S et al (2022) Brain-iot architecture and platform for building iot systems. In: Proceedings of the 7th International Conference on Internet of Things, Big Data and Security - IoTBDS, pp 67\u201377. INSTICC, SciTePress. https:\/\/doi.org\/10.5220\/0011086000003194","DOI":"10.5220\/0011086000003194"},{"issue":"3","key":"5483_CR57","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/MS.2011.27","volume":"28","author":"A Basu","year":"2011","unstructured":"Basu A, Bensalem S, Bozga M, Combaz J, Jaber M, Nguyen T-H, Sifakis J (2011) Rigorous component-based system design using the bip framework. IEEE Softw 28(3):41\u201348","journal-title":"IEEE Softw"},{"issue":"1","key":"5483_CR58","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158668","volume":"28","author":"G Agha","year":"2018","unstructured":"Agha G, Palmskog K (2018) A survey of statistical model checking. ACM Trans Model Comput Simul 28(1):1\u201339","journal-title":"ACM Trans Model Comput Simul"},{"key":"5483_CR59","doi-asserted-by":"publisher","unstructured":"Brambilla M, Cabot J, Wimmer M (2012) Model-Driven Software Engineering in Practice. 1:9. https:\/\/doi.org\/10.2200\/S00441ED1V01Y201208SWE001","DOI":"10.2200\/S00441ED1V01Y201208SWE001"},{"key":"5483_CR60","doi-asserted-by":"crossref","unstructured":"Mediouni BL, Nouri A, Bozga M, Dellabani M, Combaz J, Legay A, Bensalem S (2018) SBIP 2.0: statistical model checking stochastic real-time systems. https:\/\/www-verimag.imag.fr\/TR\/TR-2018-5.pdf","DOI":"10.1007\/978-3-030-01090-4_33"},{"key":"5483_CR61","unstructured":"Baouya A (2021) Java code generator. https:\/\/github.com\/hakimuga\/Resulted_Orchestration_Bundles"},{"key":"5483_CR62","unstructured":"CPS4EU (2019\u20132022) Cyber physical systems for Europe. https:\/\/cps4eu.eu"},{"key":"5483_CR63","unstructured":"FOCETA (2021\u20132023) Foundations for continuous engineering of trustworthy autonomy. http:\/\/www.foceta-project.eu"},{"key":"5483_CR64","unstructured":"CITADEL (2021\u20132023) Critical infrastructure protection using adaptive MILS. http:\/\/www.citadel-project.org"},{"key":"5483_CR65","unstructured":"CEA List (2019) SensiNact Gateway. Accessed 17 Jan 2020 from https:\/\/wiki.eclipse.org\/SensiNact"},{"issue":"21","key":"5483_CR66","doi-asserted-by":"publisher","first-page":"7493","DOI":"10.1016\/j.eswa.2015.05.049","volume":"42","author":"Baouya Abdelhakim","year":"2015","unstructured":"Abdelhakim Baouya, Djamal Bennouar, Ait Mohamed Otmane, Samir Ouchani (2015) A quantitative verification framework of sysml activity diagrams under time constraints. Exp Syst Appl 42(21):7493\u20137510","journal-title":"Exp Syst Appl"},{"issue":"10","key":"5483_CR67","doi-asserted-by":"publisher","first-page":"1315","DOI":"10.1109\/TC.2008.26","volume":"57","author":"S Bliudze","year":"2008","unstructured":"Bliudze S, Sifakis J (2008) The algebra of connectors-structuring interaction in BIP. IEEE Trans Comput 57(10):1315\u20131330. https:\/\/doi.org\/10.1109\/TC.2008.26","journal-title":"IEEE Trans Comput"},{"key":"5483_CR68","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer aided verification","author":"HLS Younes","year":"2002","unstructured":"Younes HLS, Simmons RG (2002) Probabilistic verification of discrete event systems using acceptance sampling. In: Ed B, Kim GL (eds) Computer aided verification. Springer, Berlin, pp 223\u2013235"},{"key":"5483_CR69","doi-asserted-by":"crossref","unstructured":"H\u00e9rault T, Lassaigne R, Magniette F, Peyronnet S (2004) Approximate probabilistic model checking. In: Verification, model checking, and abstract interpretation. Springer, Berlin, pp 73\u201384","DOI":"10.1007\/978-3-540-24622-0_8"},{"key":"5483_CR70","doi-asserted-by":"publisher","unstructured":"Dellabani M, Combaz J, Bensalem S, Bozga M (2019). Local planning semantics: a semantics for distributed real-time systems. https:\/\/doi.org\/10.4230\/LITES-v006-i001-a001","DOI":"10.4230\/LITES-v006-i001-a001"},{"key":"5483_CR71","unstructured":"Giannopoulou G et al DOL-BIP-critical: a toolchain for rigorous design and implementation of mixed-criticality multi-core systems. http:\/\/link.springer.com\/10.1007\/s10617-018-9206-3"},{"key":"5483_CR72","unstructured":"Robotnik (2020) Json file libraries for robot communication. https:\/\/github.com\/hakimuga\/Robotnik-JSON-Files"},{"key":"5483_CR73","unstructured":"ROS.org. Ros - stage. 2012. http:\/\/wiki.ros.org\/stage"},{"key":"5483_CR74","unstructured":"ROS.org. Ros - rviz. 2012. http:\/\/wiki.ros.org\/rviz"}],"container-title":["The Journal of Supercomputing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-023-05483-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11227-023-05483-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-023-05483-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,8]],"date-time":"2024-01-08T11:31:06Z","timestamp":1704713466000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11227-023-05483-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,12]]},"references-count":74,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,1]]}},"alternative-id":["5483"],"URL":"https:\/\/doi.org\/10.1007\/s11227-023-05483-x","relation":{},"ISSN":["0920-8542","1573-0484"],"issn-type":[{"value":"0920-8542","type":"print"},{"value":"1573-0484","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,7,12]]},"assertion":[{"value":"6 June 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 July 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"This article does not contain any studies with human participants or animals performed by any of the authors.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical approval"}},{"value":"Informed consent was obtained from all individual participants included in the study.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Informed consent"}}]}}