{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,6]],"date-time":"2026-07-06T20:01:38Z","timestamp":1783368098497,"version":"3.54.6"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2024,7,17]],"date-time":"2024-07-17T00:00:00Z","timestamp":1721174400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,7,17]],"date-time":"2024-07-17T00:00:00Z","timestamp":1721174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["SN COMPUT. SCI."],"DOI":"10.1007\/s42979-024-03027-5","type":"journal-article","created":{"date-parts":[[2024,7,17]],"date-time":"2024-07-17T13:01:52Z","timestamp":1721221312000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Incremental and Formal Verification of SysML Models"],"prefix":"10.1007","volume":"5","author":[{"given":"Sophie","family":"Coudert","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ludovic","family":"Apvrille","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bastien","family":"Sultan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6612-8574","authenticated-orcid":false,"given":"Oana","family":"Hotescu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pierre","family":"de Saqui-Sannes","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,7,17]]},"reference":[{"key":"3027_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial JR. Modeling in Event-B: System and Software Engineering. 1st ed. USA: Cambridge University Press; 2010.","edition":"1"},{"key":"3027_CR2","doi-asserted-by":"crossref","unstructured":"Aichernig BK, Lorber F, Ni\u010dkovi\u0107 D. Time for mutants\u2013model-based mutation testing with timed automata. In: International Conference on Tests and Proofs, Springer, 2013;pp 20\u201338","DOI":"10.1007\/978-3-642-38916-0_2"},{"issue":"6","key":"3027_CR3","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s11334-018-0318-5","volume":"14","author":"S Ali","year":"2018","unstructured":"Ali S. Formal verification of SysML diagram using case studies of real-time system. Innovations Syst Softw Eng. 2018;14(6):245\u201362. https:\/\/doi.org\/10.1007\/s11334-018-0318-5.","journal-title":"Innovations Syst Softw Eng"},{"key":"3027_CR4","doi-asserted-by":"crossref","unstructured":"Alparslan O, Arakawa S, Murata M. A zone-based optical intra-vehicle backbone network architecture with dynamic slot scheduling. Optical Switching and Networking 2023;p 100753","DOI":"10.1016\/j.osn.2023.100753"},{"key":"3027_CR5","doi-asserted-by":"publisher","unstructured":"Ando T, Yatsu H, Kong W, et\u00a0al. Formalization and model checking of SysML state machine diagrams by csp#. In: Computational Science and Its Applications (ICCSA), 2013;p 114-127, https:\/\/doi.org\/10.1007\/978-3-642-39646-5_9","DOI":"10.1007\/978-3-642-39646-5_9"},{"key":"3027_CR6","doi-asserted-by":"publisher","unstructured":"Apvrille L, de\u00a0Saqui-Sannes P. Analysis Techniques to Verify Mutual Exclusion Situations within SysML Models. In: SDL 2013: Model-Driven Dependability Engineering. SDL 2013. Lecture Notes in Computer Science, vol 7916. Springer, Berlin, Heidelberg, 2013. https:\/\/doi.org\/10.1007\/978-3-642-38911-5_6","DOI":"10.1007\/978-3-642-38911-5_6"},{"issue":"7","key":"3027_CR7","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1109\/TSE.2004.34","volume":"30","author":"L Apvrille","year":"2004","unstructured":"Apvrille L, Courtiat JP, Lohr C, et al. TURTLE: A real-time UML profile supported by a formal validation toolkit. IEEE Trans Software Eng. 2004;30(7):473\u201387.","journal-title":"IEEE Trans Software Eng"},{"key":"3027_CR8","doi-asserted-by":"publisher","unstructured":"Apvrille L, de\u00a0Saqui-Sannes P, Hotescu O, et\u00a0al. SysML Models Verification Relying on Dependency Graphs. In: 10th International Conference on Model-Driven Engineering and Software Development, Vienna, Austria, 2022.https:\/\/doi.org\/10.5220\/0010792900003119, https:\/\/hal.telecom-paris.fr\/hal-03575960","DOI":"10.5220\/0010792900003119"},{"key":"3027_CR9","doi-asserted-by":"crossref","unstructured":"Apvrille L, Sultan B, Hotescu O, et\u00a0al. Mutation of Formally Verified SysML Models. In: 11th internationl conference on Model-Based Software and Systems Engineering (Modelsward\u20192023) 2023.","DOI":"10.5220\/0011648300003402"},{"key":"3027_CR10","doi-asserted-by":"publisher","unstructured":"Bougacha R, Laleau R, Collart-Dutilleul S, et\u00a0al. Extending SysML with Refinement and Decomposition Mechanisms to Generate Event-B Specifications. In: TASE 2022: Theoretical Aspects of Software Engineering, Lecture Notes in Computer Science, vol 13299. Springer, 2022;pp 256\u2013273, https:\/\/doi.org\/10.1007\/978-3-540-88387-6","DOI":"10.1007\/978-3-540-88387-6"},{"key":"3027_CR11","unstructured":"Calvino AT, Apvrille L. Direct model-checking of SysML models. In: Proceedings of the 9th International Conference on Model-Driven Engineering and Software Development (Modelsward\u20192021), Vienna, Autrichia (online) 2021."},{"key":"3027_CR12","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-319-07602-7_7","volume-title":"Formal Aspects of Component Software (FACS 2013","author":"O Carrillo","year":"2014","unstructured":"Carrillo O, Chouali S, Mountassir H. Incremental Modeling of System Architecture Satisfying SysML Functional Requirements. In: Fiadeiro JL, Liu Z, Xue J, editors. Formal Aspects of Component Software (FACS 2013. Lecture Notes in Computer Science: Springer; 2014. p. 79\u201399."},{"key":"3027_CR13","doi-asserted-by":"publisher","unstructured":"Delatour J, Paludetto M. UML\/PNO: A way to merge UML and Petri net objects for the analysis of real-time systems. In: Oriented Technology: ECOOP\u201998 Workshop Reader, 1998;p 511-514, https:\/\/doi.org\/10.1007\/3-540-49255-0_169","DOI":"10.1007\/3-540-49255-0_169"},{"key":"3027_CR14","doi-asserted-by":"crossref","unstructured":"Fisman D, Pnueli A. Beyond regular model checking. 21st conference on Foundations of Software Technology and Theoretical Computer Science LNCS 2245, 2001.","DOI":"10.1007\/3-540-45294-X_14"},{"issue":"22","key":"3027_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1002\/sys21679","volume":"1","author":"B Horv\u00e1th","year":"2023","unstructured":"Horv\u00e1th B, Moln\u00e1r V, Graics B, et al. Pragmatic verification and validation of industrial executable sysml models. Syst Eng. 2023;1(22):1\u201322. https:\/\/doi.org\/10.1002\/sys21679.","journal-title":"Syst Eng"},{"issue":"1","key":"3027_CR16","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1002\/sys.21524","volume":"23","author":"E Huang","year":"2019","unstructured":"Huang E, McGinnis L, Mitchell S. Verifying sysml activity diagrams using formal transformation to Petri nets. Syst Eng. 2019;23(1):118\u201335.","journal-title":"Syst Eng"},{"key":"3027_CR17","unstructured":"IEEE. 802.1Q - IEEE Standard for Local and Metropolitan Area Networks-Bridges and Bridged Networks. https:\/\/standardsieeeorg\/standard\/802 1Q-2018html (2018)."},{"key":"3027_CR18","unstructured":"Kausch1 M, Pfeiffer1, Raco1 D, et al. Model-based design of correct safety-critical systems using dataflow languages on the example of SysML architecture and behavior diagrams. In: AVIOSE\u20192021, Software Engineering 2021 Satellite Events. Germany (virtual), Lecture Notes in Informatics (LNI), Gesellschaft f\u00fcr Informatik: Bonn; 2021. p. 1\u201322."},{"key":"3027_CR19","doi-asserted-by":"publisher","DOI":"10.4271\/2021-01-0260","author":"M Mahani","year":"2021","unstructured":"Mahani M, Rizzo D, Paredis C, et al. Automatic formal verification of SysML state machine diagrams for vehicular control system. SAE Technical Paper. 2021. https:\/\/doi.org\/10.4271\/2021-01-0260.","journal-title":"SAE Technical Paper"},{"key":"3027_CR20","doi-asserted-by":"crossref","unstructured":"Neumann R. Using Promela in a Fully Verified Executable LTL Model Checker. In: Working Conference on Verified Software: Theories, Tools, and Experiments, Springer, 2014;pp 105\u2013114.","DOI":"10.1007\/978-3-319-12154-3_7"},{"key":"3027_CR21","unstructured":"OMG. OMG Systems Modeling Language. Object Management Group, https:\/\/www.omg.org\/spec\/SysML\/1.5 2017."},{"key":"3027_CR22","doi-asserted-by":"publisher","unstructured":"Ouchani S, Ait\u00a0Mohamed O, Debbabi M. A formal verification framework for SysML activity diagrams. Expert Systems with Applications. 2014; 41(6). https:\/\/doi.org\/10.1016\/j.eswa.2013.10.064","DOI":"10.1016\/j.eswa.2013.10.064"},{"issue":"2","key":"3027_CR23","doi-asserted-by":"publisher","first-page":"669","DOI":"10.3390\/s23020669","volume":"23","author":"C Park","year":"2023","unstructured":"Park C, Park S. Performance evaluation of zone-based in-vehicle network architecture for autonomous vehicles. Sensors. 2023;23(2):669.","journal-title":"Sensors"},{"key":"3027_CR24","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/s11334-016-0281-y","volume":"13","author":"M Rahim","year":"2017","unstructured":"Rahim M, Hammad A, Ioualalen M. A methodology for verifying SysML requirements using activity diagrams. Innovations Syst Softw Eng. 2017;13:19\u201333.","journal-title":"Innovations Syst Softw Eng"},{"key":"3027_CR25","doi-asserted-by":"crossref","unstructured":"Rahim M, Boukala-Loualalen M, Hammad A. Hierarchical colored Petri nets for the verification of SysML designs - activity-based slicing approach. In: 4th Conf. on Computing Systems and Appli. (CSA 2020), Algiers, Algeria, 2020;pp 131\u2013142, https:\/\/publiweb.femto-st.fr\/tntnet\/entries\/17274\/documents\/author\/data","DOI":"10.1007\/978-3-030-69418-0_12"},{"key":"3027_CR26","first-page":"1","volume-title":"12th International Conference on Modeling, Optimisation and Simulation (Mosim 2018)","author":"P de Saqui-Sannes","year":"2018","unstructured":"de Saqui-Sannes P, Vingerhoeds R, Apvrille L. Early checking of SysML models applied to protocols. In: 12th International Conference on Modeling, Optimisation and Simulation (Mosim 2018). France: Toulouse; 2018. p. 1\u20138."},{"key":"3027_CR27","doi-asserted-by":"crossref","unstructured":"de\u00a0Saqui-Sannes P, Apvrille L, Vingerhoeds RA. Checking SysML Models against Safety and Security Properties. Journal of Aerospace Information Systems 2021;pp 1\u201313.","DOI":"10.2514\/1.I010950"},{"key":"3027_CR28","doi-asserted-by":"publisher","first-page":"120936","DOI":"10.1109\/ACCESS.2022.3222387","volume":"10","author":"P de Saqui-Sannes","year":"2022","unstructured":"de Saqui-Sannes P, Vingerhoeds RA, Garion C, et al. A taxonomy of MBSE approaches by languages, tools and methods. IEEE Access. 2022;10:120936\u201350. https:\/\/doi.org\/10.1109\/ACCESS.2022.3222387.","journal-title":"IEEE Access"},{"key":"3027_CR29","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1016\/S1571-0661(04)00262-2","volume":"55","author":"T Schafer","year":"2001","unstructured":"Schafer T, Knapp A, Merz S. Model checking UML state machines and collaborations. Electronic Notes in Theoretical Computer Science. 2001;55:357\u201369. https:\/\/doi.org\/10.1016\/S1571-0661(04)00262-2.","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"3027_CR30","doi-asserted-by":"publisher","first-page":"76351","DOI":"10.1109\/ACCESS.2022.3192436","volume":"10","author":"FG Rey de Souza","year":"2022","unstructured":"Rey de Souza FG, Hirata CM, Nadjm-Tehrani S. Synthesis of a controller algorithm for safety-critical systems. IEEE Access. 2022;10:76351\u201375. https:\/\/doi.org\/10.1109\/ACCESS.2022.3192436.","journal-title":"IEEE Access"},{"key":"3027_CR31","doi-asserted-by":"crossref","unstructured":"Staskal O, Simac J, Swayne L, et\u00a0al. Translating sysml activity diagrams for nuxmv verification of an autonomous pancreas. In: SESS22), 2022;pp 1\u20136.","DOI":"10.1109\/COMPSAC54236.2022.00260"},{"key":"3027_CR32","doi-asserted-by":"crossref","unstructured":"Sultan B, Apvrille L, Jaillon P, et\u00a0al. W-Sec: a Model-Based Formal Method for Assessing the Impacts of Security Countermeasures. In: International Conference on Model-Driven Engineering and Software Development, Springer, 2021; pp 203\u2013229.","DOI":"10.1007\/978-3-031-38821-7_10"},{"key":"3027_CR33","doi-asserted-by":"crossref","unstructured":"Sultan B, Fr\u00e9not L, Apvrille L, et\u00a0al. AMULET: a Mutation Language Enabling Automatic Enrichment of SysML Models. ACM Transactions on Embedded Computing Systems, 2023.","DOI":"10.1145\/3624583"},{"key":"3027_CR34","doi-asserted-by":"publisher","unstructured":"Szmuc W, Szmuc T. Towards embedded systems formal verification translation from SysML into Petri nets. In: 25th International Conference Mixed Design of Integrated Circuits and System (MIXDES), 2018;pp 420\u2013423, https:\/\/doi.org\/10.23919\/MIXDES.2018.843687","DOI":"10.23919\/MIXDES.2018.843687"},{"key":"3027_CR35","unstructured":"TTool (2022) https:\/\/ttool.telecom-paris.fr\/. Retrieved May 11, 2022"},{"issue":"1","key":"3027_CR36","first-page":"3","volume":"5","author":"J Von Neumann","year":"1966","unstructured":"Von Neumann J, Burks AW, et al. Theory of self-reproducing automata. IEEE Trans Neural Networks. 1966;5(1):3\u201314.","journal-title":"IEEE Trans Neural Networks"},{"key":"3027_CR37","doi-asserted-by":"publisher","unstructured":"Wang H, Zhong D, Zhao T, et al. Integrating model checking with sysml in complex system safety analysis. IEEE Access. 2019;7:16561\u201371. https:\/\/doi.org\/10.1109\/ACCESS.2019.2892745.","DOI":"10.1109\/ACCESS.2019.2892745"},{"key":"3027_CR38","doi-asserted-by":"publisher","unstructured":"Xie J, Tan W, Yang Z, et al. Sysml-based compositional verification and safety analysis for safety-critical cyber-physical systems. Connect Sci. 2022;34(1):911\u201341. https:\/\/doi.org\/10.1080\/09540091.2021.2017853.","DOI":"10.1080\/09540091.2021.2017853"}],"container-title":["SN Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42979-024-03027-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s42979-024-03027-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42979-024-03027-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T08:23:34Z","timestamp":1732436614000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s42979-024-03027-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,17]]},"references-count":38,"journal-issue":{"issue":"6","published-online":{"date-parts":[[2024,8]]}},"alternative-id":["3027"],"URL":"https:\/\/doi.org\/10.1007\/s42979-024-03027-5","relation":{},"ISSN":["2661-8907"],"issn-type":[{"value":"2661-8907","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,7,17]]},"assertion":[{"value":"14 July 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 June 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 July 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"On behalf of all authors, the corresponding author states that there is no Conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"714"}}