{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T07:29:38Z","timestamp":1743146978372,"version":"3.40.3"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031388200"},{"type":"electronic","value":"9783031388217"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-38821-7_6","type":"book-chapter","created":{"date-parts":[[2023,8,3]],"date-time":"2023-08-03T15:02:10Z","timestamp":1691074930000},"page":"109-134","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Dependency Graphs to\u00a0Boost the\u00a0Verification of\u00a0SysML Models"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1167-4639","authenticated-orcid":false,"given":"Ludovic","family":"Apvrille","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1404-0148","authenticated-orcid":false,"given":"Pierre","family":"de Saqui-Sannes","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6612-8574","authenticated-orcid":false,"given":"Oana","family":"Hotescu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1312-2907","authenticated-orcid":false,"given":"Alessandro Tempia","family":"Calvino","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,8,4]]},"reference":[{"issue":"6","key":"6_CR1","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. 14(6), 245\u2013262 (2018). https:\/\/doi.org\/10.1007\/s11334-018-0318-5","journal-title":"Innovations Syst. Softw. Eng."},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Ando, T., Yatsu, H., Kong, W., Hisazumi, K., Fukuda, A.: Formalization and model checking of SysML state machine diagrams by csp#. In: Computational Science and Its Applications (ICCSA), pp. 114\u2013127 (2013). https:\/\/doi.org\/10.1007\/978-3-642-39646-5_9","DOI":"10.1007\/978-3-642-39646-5_9"},{"key":"6_CR3","doi-asserted-by":"publisher","unstructured":"Apvrille, L., de Saqui-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":"6_CR4","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1109\/TSE.2004.34","volume":"30","author":"L Apvrille","year":"2004","unstructured":"Apvrille, L., Courtiat, J.P., Lohr, C., de Saqui-Sannes, P.: TURTLE: a real-time UML profile supported by a formal validation toolkit. IEEE Trans. Software Eng. 30(7), 473\u2013487 (2004)","journal-title":"IEEE Trans. Software Eng."},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Apvrille, L., de Saqui-Sannes, P., Hotescu, O., Calvino, A.T.: 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:\/\/telecom-paris.hal.science\/hal-03575960","DOI":"10.5220\/0010792900003119"},{"issue":"2","key":"6_CR6","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1109\/JMASS.2020.3013325","volume":"1","author":"L Apvrille","year":"2020","unstructured":"Apvrille, L., de Saqui-Sannes, P., Vingerhoeds, R.A.: An educational case study of using SysML and ttool for unmanned aerial vehicles design. IEEE J. Miniaturization Air Space Syst. 1(2), 117\u2013129 (2020)","journal-title":"IEEE J. Miniaturization Air Space Syst."},{"key":"6_CR7","doi-asserted-by":"publisher","unstructured":"Ayache, J.M., Courtiat, J.P., Diaz, M.: Rebus, a fault-tolerant distributed system for industrial real-time control. IEEE Trans. Comput. C-31(7), 637\u2013647 (July 1982). https:\/\/doi.org\/10.1109\/TC.1982.1676061","DOI":"10.1109\/TC.1982.1676061"},{"key":"6_CR8","unstructured":"Baduel, R., Chami, M., Bruel, J.-M., Ober, I.: Validation in an industrial context: Challenges and experimentation. In: European Conference on Modelling Foundations and Applications, Toulouse, France (June 2021)"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Bourdil, P., Berthomieu, B., Dal Zilio, S., Vernadat, F.: Symmetry reduced state classes for time Petri nets. In: 30th Annual ACM Symposium on Applied Computing), pp. 1751\u20131758. ACM (2015)","DOI":"10.1145\/2695664.2695803"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Brisacier-Porchon, L., Hammami, O., Boutemy, R.: Modeling a uav in practice: A comparison between rhapsody and capella. In: IEEE International Symposium on Systems Engineering (ISSE), pp. 1\u20138 (2021). https:\/\/doi.org\/10.1109\/ISSE51541.2021.9582553","DOI":"10.1109\/ISSE51541.2021.9582553"},{"key":"6_CR11","unstructured":"Calvino, A.T., 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":"6_CR12","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. pp. 511\u2013514 (1998). https:\/\/doi.org\/10.1007\/3-540-49255-0_169","DOI":"10.1007\/3-540-49255-0_169"},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"Dragomir, I., Ober, I., Percebois, C.: Contract-based modeling and verification of timed safety requirements within sysml. Softw. Syst. Model. 16(2), 587\u2013624 (2017). https:\/\/doi.org\/10.1007\/s10270-015-0481-1","DOI":"10.1007\/s10270-015-0481-1"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Farzaneh, M.H., Kugele, S., Knoll, A.: A graphical modeling tool supporting automated schedule synthesis for time-sensitive networking. In: 2017 22nd IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), pp. 1\u20138. IEEE (2017)","DOI":"10.1109\/ETFA.2017.8247599"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Gao, H., Dai, B., Miao, H., Yang, X., Duran Barroso, R.J., Walayat, H.: A novel gapg approach to automatic property generation for formal verification: The gan perspective. ACM Transactions on Multimedia Computing, Communications, and Applications (February 2022). https:\/\/doi.org\/10.1145\/3517154","DOI":"10.1145\/3517154"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Guo, W., Huang, Y., Shi, J., Hou, Z., Yang, Y.: A formal method for evaluating the performance of tsn traffic shapers using uppaal. In: 2021 IEEE 46th Conference on Local Computer Networks (LCN), pp. 241\u2013248. IEEE (2021)","DOI":"10.1109\/LCN52139.2021.9524955"},{"key":"6_CR17","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley (2004)"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Hotescu, O., Jaffr\u00e8s-Runser, K., Scharbarg, J.L., Fraboul, C.: Multiplexing avionics and additional flows on a qos-aware AFDX network. In: 2019 24th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), pp. 282\u2013289. IEEE (2019)","DOI":"10.1109\/ETFA.2019.8869506"},{"issue":"1","key":"6_CR19","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. 23(1), 118\u2013135 (2019)","journal-title":"Syst. Eng."},{"key":"6_CR20","unstructured":"IEEE: IEEE Standard for Local and metropolitan area networks-Frame Replication and Elimination for Reliability (2017)"},{"key":"6_CR21","unstructured":"IEEE: 802.1Q - IEEE Standard for Local and Metropolitan Area Networks-Bridges and Bridged Networks. www.standards.ieee.org\/ standard\/802 1Q\u20132018.html (2018)"},{"key":"6_CR22","doi-asserted-by":"publisher","unstructured":"Kaleeswaran, A., Nordmann, A., Vogel, T., Grunske, L.: A systematic literature review on counterexample explanation. Inform. Softw. Technol. 145 (2022). https:\/\/doi.org\/10.1016\/j.infsof.2021.106800","DOI":"10.1016\/j.infsof.2021.106800"},{"key":"6_CR23","unstructured":"Kausch1, M., Pfeiffer1, Raco1, D., Rumpe, B.: 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, Bonn, Germany (virtual), pp. 1\u201322. Lecture Notes in Informatics (LNI), Gesellschaft f\u00fcr Informatik (2021)"},{"key":"6_CR24","doi-asserted-by":"publisher","first-page":"91710","DOI":"10.1109\/ACCESS.2021.3092572","volume":"9","author":"W Kong","year":"2021","unstructured":"Kong, W., Nabi, M., Goossens, K.: Run-time recovery and failure analysis of time-triggered traffic in time sensitive networks. IEEE Access 9, 91710\u201391722 (2021)","journal-title":"IEEE Access"},{"key":"6_CR25","doi-asserted-by":"publisher","unstructured":"Laleau, R., Mammar, A.: An overview of a method and its support tool for generating B specifications from UML notations. In: ASE2000. Fifteenth IEEE International Conference on Automated Software Engineering, pp. 269\u2013272 (2000). https:\/\/doi.org\/10.1109\/ASE.2000.873675","DOI":"10.1109\/ASE.2000.873675"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Leroux-Beaudout, R., Pantel, M., Ober, I., Bruel, J.M.: Model-based systems engineering for systems simulation. In: Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018), Limassol, Cyprus (2018)","DOI":"10.1007\/978-3-030-03424-5_29"},{"issue":"3","key":"6_CR27","doi-asserted-by":"publisher","first-page":"1286","DOI":"10.1109\/TR.2020.3026689","volume":"70","author":"J Lv","year":"2020","unstructured":"Lv, J., Zhao, Y., Wu, X., Li, Y., Wang, Q.: Formal analysis of tsn scheduler for real-time communications. IEEE Trans. Reliab. 70(3), 1286\u20131294 (2020)","journal-title":"IEEE Trans. Reliab."},{"key":"6_CR28","doi-asserted-by":"publisher","DOI":"10.4271\/2021-01-0260","author":"M Mahani","year":"2021","unstructured":"Mahani, M., Rizzo, D., Paredis, C., Wang, Y.: Automatic formal verification of SysML state machine diagrams for vehicular control system. SAE Tech. Paper (2021). https:\/\/doi.org\/10.4271\/2021-01-0260","journal-title":"SAE Tech. Paper"},{"key":"6_CR29","unstructured":"Modeler, C.S.: www.3ds.com\/products-services\/catia\/products\/no-magic\/cameo-systems-modeler\/ Retrieved May 16 2022 (2022)"},{"key":"6_CR30","unstructured":"OMG: OMG Systems Modeling Language. Object Management Group, www.omg.org\/spec\/SysML\/1.5 (2017)"},{"key":"6_CR31","doi-asserted-by":"publisher","unstructured":"Ouchani, S., Ait Mohamed, O., Debbabi, M.: A formal verification framework for SysML activity diagrams. Expert Syst. Appl. 41(6) (2014). https:\/\/doi.org\/10.1016\/j.eswa.2013.10.064","DOI":"10.1016\/j.eswa.2013.10.064"},{"key":"6_CR32","unstructured":"Papyrus: www.eclipse.org\/papyrus\/ Retrieved May 16 2022 (2022)"},{"key":"6_CR33","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 Conference on Computing Systems and Appli. (CSA 2020). Lecture Notes in Networks and Systems, vol. 199, pp. 131\u2013142. Algiers, Algeria (dec 2020), www.publiweb.femto-st.fr\/tntnet\/entries\/17274\/documents\/author\/data","DOI":"10.1007\/978-3-030-69418-0_12"},{"key":"6_CR34","unstructured":"Rhapsody: www.ibm.com\/fr-fr\/products\/architect-for-systems-engineers Retrieved May 16 2022 (2022)"},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"Samson, M., Vergnaud, T., Dujardin, \u00c9., Ciarletta, L., Song, Y.Q.: A model-based approach to automatic generation of tsn network simulations. In: 2022 IEEE 18th International Conference on Factory Communication Systems (WFCS), pp. 1\u20138. IEEE (2022)","DOI":"10.1109\/WFCS53837.2022.9779173"},{"key":"6_CR36","doi-asserted-by":"crossref","unstructured":"de Saqui-Sannes, P., Apvrille, L., Vingerhoeds, R.A.: Checking SysML Models against Safety and Security Properties. Journal of Aerospace Information Systems pp. 1\u201313 (Nov 2021)","DOI":"10.2514\/1.I010950"},{"key":"6_CR37","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. Electron. Notes Theor. Comput. Sci. 55, 357\u2013369 (2001). https:\/\/doi.org\/10.1016\/S1571-0661(04)00262-2","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"6_CR38","doi-asserted-by":"publisher","unstructured":"de Souza, F.G.R., de Melo Bezerra, J., Hirata, C.M., de Saqui-Sannes, P., Apvrille, L.: Combining stpa with sysml modeling. In: IEEE International Systems Conference (SysCon), pp. 1\u20138 (2020). https:\/\/doi.org\/10.1109\/SysCon47679.2020.9275867","DOI":"10.1109\/SysCon47679.2020.9275867"},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"Staskal, O., Simac, J., Swayne, L., Rozier, K.Y.: Translating sysml activity diagrams for nuxmv verification of an autonomous pancreas. In: SESS22), pp. 1\u20136 (2022)","DOI":"10.1109\/COMPSAC54236.2022.00260"},{"key":"6_CR40","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), pp. 420\u2013423 (2018). https:\/\/doi.org\/10.23919\/MIXDES.2018.843687","DOI":"10.23919\/MIXDES.2018.843687"},{"key":"6_CR41","doi-asserted-by":"crossref","unstructured":"Thomas, L., Mifdaoui, A., Boudec, J.Y.L.: Worst-case delay bounds in time-sensitive networks with packet replication and elimination. arXiv preprint arXiv:2110.05808 (2021)","DOI":"10.1109\/TNET.2022.3180763"},{"key":"6_CR42","unstructured":"TINA: Time Petri net analyzer. www.projects.laas.fr\/tina\/\/ Retrieved October 31 2020 (2020)"},{"key":"6_CR43","unstructured":"TTool: www.ttool.telecom-paris.fr\/ Retrieved May 11 2022 (2022)"},{"key":"6_CR44","doi-asserted-by":"publisher","first-page":"16561","DOI":"10.1109\/ACCESS.2019.2892745","volume":"7","author":"H Wang","year":"2019","unstructured":"Wang, H., Zhong, D., Zhao, T., Ren, F.: Integrating model checking with sysml in complex system safety analysis. IEEE Access 7, 16561\u201316571 (2019). https:\/\/doi.org\/10.1109\/ACCESS.2019.2892745","journal-title":"IEEE Access"},{"issue":"5","key":"6_CR45","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3458768","volume":"20","author":"Y Zhou","year":"2021","unstructured":"Zhou, Y., Samii, S., Eles, P., Peng, Z.: Reliability-aware scheduling and routing for messages in time-sensitive networking. ACM Trans. Embedded Comput. Syst. (TECS) 20(5), 1\u201324 (2021)","journal-title":"ACM Trans. Embedded Comput. Syst. (TECS)"},{"key":"6_CR46","doi-asserted-by":"crossref","unstructured":"Zoor, M., Apvrille, L., Pacalet, R.: Execution Trace Analysis for a Precise Understanding of Latency Violations. In: International Conference on Model Driven Engineering Languages and Systems (MODELS). Fukuoka (virtual), Japan (Oct 2021). https:\/\/telecom-paris.hal.science\/hal-03349254","DOI":"10.1109\/MODELS50736.2021.00021"}],"container-title":["Communications in Computer and Information Science","Model-Driven Engineering and Software Development"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-38821-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,3]],"date-time":"2023-08-03T15:05:28Z","timestamp":1691075128000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-38821-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031388200","9783031388217"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-38821-7_6","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"4 August 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"MODELSWARD","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Model-Driven Engineering and Software Development","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 February 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 February 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"modelsward2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/modelsward.scitevents.org\/?y=2022","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"PRIMORIS","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"59","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"17% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}