{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,2]],"date-time":"2025-07-02T09:25:07Z","timestamp":1751448307794,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031781155"},{"type":"electronic","value":"9783031781162"}],"license":[{"start":{"date-parts":[[2024,11,29]],"date-time":"2024-11-29T00:00:00Z","timestamp":1732838400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,29]],"date-time":"2024-11-29T00:00:00Z","timestamp":1732838400000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-78116-2_6","type":"book-chapter","created":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T07:31:51Z","timestamp":1732779111000},"page":"86-104","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["An Integrated Framework for\u00a0Analysing, Simulating and\u00a0Testing UML Models"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3700-9709","authenticated-orcid":false,"given":"Gustavo","family":"Carvalho","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1320-5262","authenticated-orcid":false,"given":"Jos\u00e9","family":"Dihego","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6593-577X","authenticated-orcid":false,"given":"Augusto","family":"Sampaio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,29]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, E., Liu, S., Liu, Y., Choppy, C., Sun, J., Dong, J.S.: Formalizing UML state machines for automated verification - a survey. ACM Comput. Surv. 55(13s) (2023). https:\/\/doi.org\/10.1145\/3579821","DOI":"10.1145\/3579821"},{"key":"6_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"key":"6_CR3","volume-title":"The Unified Modeling Language User Guide","author":"G Booch","year":"1999","unstructured":"Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Addison-Wesley, Reading (1999)"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Calvino., A., Apvrille., L.: Direct model-checking of SysML models. In: Proceedings of the 9th International Conference on Model-Driven Engineering and Software Development - MODELSWARD, pp. 216\u2013223. INSTICC, SciTePress (2021). https:\/\/doi.org\/10.5220\/0010256302160223","DOI":"10.5220\/0010256302160223"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-319-22969-0_20","volume-title":"Software Engineering and Formal Methods","author":"G Carvalho","year":"2015","unstructured":"Carvalho, G., Barros, F., Carvalho, A., Cavalcanti, A., Mota, A., Sampaio, A.: NAT2TEST tool: from natural language requirements to test cases based on CSP. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 283\u2013290. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22969-0_20"},{"issue":"5","key":"6_CR6","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1007\/s00165-016-0387-x","volume":"28","author":"G Carvalho","year":"2016","unstructured":"Carvalho, G., Cavalcanti, A., Sampaio, A.: Modelling timed reactive systems from natural-language requirements. Form. Asp. Comput. 28(5), 725\u2013765 (2016). https:\/\/doi.org\/10.1007\/s00165-016-0387-x","journal-title":"Form. Asp. Comput."},{"key":"6_CR7","unstructured":"Carvalho, G., Dihego, J., Sampaio, A.: Artefact associated with this paper: \u201can integrated framework for analysing, simulating and testing UML models\u201d (2024). https:\/\/zenodo.org\/doi\/10.5281\/zenodo.13323735"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"Carvalho, G., Meira, I.: Validating, verifying and testing timed data-flow reactive systems in Coq from controlled natural-language requirements. Sci. Comput. Program. 201, 102537 (2021). https:\/\/doi.org\/10.1016\/j.scico.2020.102537, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0167642320301453","DOI":"10.1016\/j.scico.2020.102537"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-41202-8_11","volume-title":"Formal Methods and Software Engineering","author":"G Carvalho","year":"2013","unstructured":"Carvalho, G., Sampaio, A., Mota, A.: A CSP timed input-output relation and a strategy for mechanised conformance verification. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 148\u2013164. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41202-8_11"},{"key":"6_CR10","unstructured":"Change Vision, Inc.: Astah UML User\u2019s Guide (nd). https:\/\/astah.net\/support\/astah-uml\/. Accessed 25 June 2024"},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"Chen, Z., Liu, Z., Ravn, A.P., Stolz, V., Zhan, N.: Refinement and verification in component-based model-driven design. Sci. Comput. Program. 74(4), 168\u2013196 (2009). https:\/\/doi.org\/10.1016\/j.scico.2008.08.003, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0167642308000890. Special Issue on the Grand Challenge","DOI":"10.1016\/j.scico.2008.08.003"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Cicchetti, A., et sl.: CHESS: a model-driven engineering tool environment for aiding the development of complex industrial systems. In: 2012 Proceedings of the 27th IEEE\/ACM International Conference on Automated Software Engineering, pp. 362\u2013365 (2012). https:\/\/doi.org\/10.1145\/2351676.2351748","DOI":"10.1145\/2351676.2351748"},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"Ciccozzi, F., Malavolta, I., Selic, B.: Execution of UML models: a systematic review of research and practice. Softw. Syst. Model. 18(3), 2313\u20132360 (2019). https:\/\/doi.org\/10.1007\/s10270-018-0675-4","DOI":"10.1007\/s10270-018-0675-4"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"6_CR15","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1145\/365559.365617","volume":"8","author":"EW Dijkstra","year":"1965","unstructured":"Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8, 569 (1965). https:\/\/doi.org\/10.1145\/365559.365617","journal-title":"Commun. ACM"},{"issue":"8","key":"6_CR16","doi-asserted-by":"publisher","first-page":"2124","DOI":"10.1109\/TSE.2024.3422845","volume":"50","author":"M Elekes","year":"2024","unstructured":"Elekes, M., Moln\u00e1r, V., Micskei, Z.: To do or not to do: semantics and patterns for do activities in UML PSSM state machines. IEEE Trans. Softw. Eng. 50(8), 2124\u20132141 (2024). https:\/\/doi.org\/10.1109\/TSE.2024.3422845","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"3","key":"6_CR17","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1007\/S10270-023-01127-Z","volume":"23","author":"F Falc\u00e3o","year":"2024","unstructured":"Falc\u00e3o, F., Lima, L., Sampaio, A., Antonino, P.: A formal component model for UML based on CSP aiming at compositional verification. Softw. Syst. Model. 23(3), 765\u2013798 (2024). https:\/\/doi.org\/10.1007\/S10270-023-01127-Z","journal-title":"Softw. Syst. Model."},{"issue":"6","key":"6_CR18","doi-asserted-by":"publisher","first-page":"1483","DOI":"10.1007\/s10270-020-00806-5","volume":"19","author":"B Graics","year":"2020","unstructured":"Graics, B., Moln\u00e1r, V., V\u00f6r\u00f6s, A., Majzik, I., Varr\u00f3, D.: Mixed-semantics composition of statecharts for the component-based design of reactive systems. Softw. Syst. Model. 19(6), 1483\u20131517 (2020). https:\/\/doi.org\/10.1007\/s10270-020-00806-5","journal-title":"Softw. Syst. Model."},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-031-52183-6_2","volume-title":"Formal Aspects of Component Software","author":"B Graics","year":"2024","unstructured":"Graics, B., Mondok, M., Moln\u00e1r, V., Majzik, I.: Model-based testing of asynchronously communicating distributed controllers. In: C\u00e1mara, J., Jongmans, S.S. (eds.) FACS 2023. LNCS, vol. 14485, pp. 23\u201344. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-52183-6_2"},{"key":"6_CR20","unstructured":"Hoare, C.: Communicating Sequential Processes. Prentice-Hall International (1985)"},{"key":"6_CR21","doi-asserted-by":"publisher","unstructured":"Horv\u00e1th, B., et al.: Pragmatic verification and validation of industrial executable SysML models. Syst. Eng. 26(6), 693\u2013714 (2023). https:\/\/doi.org\/10.1002\/sys.21679, https:\/\/incose.onlinelibrary.wiley.com\/doi\/abs\/10.1002\/sys.21679","DOI":"10.1002\/sys.21679"},{"key":"6_CR22","unstructured":"Lampropoulos, L., Pierce, B.C.: QuickChick: Property-Based Testing in Coq, Software Foundations, vol.\u00a04. Electronic textbook (2023). http:\/\/softwarefoundations.cis.upenn.edu. Version 1.3.2"},{"issue":"3","key":"6_CR23","doi-asserted-by":"publisher","first-page":"875","DOI":"10.1007\/s10270-015-0492-y","volume":"16","author":"L Lima","year":"2017","unstructured":"Lima, L., et al.: An integrated semantics for reasoning about SysML design models using refinement. Softw. Syst. Model. 16(3), 875\u2013902 (2017). https:\/\/doi.org\/10.1007\/s10270-015-0492-y","journal-title":"Softw. Syst. Model."},{"issue":"6","key":"6_CR24","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1109\/TSE.2012.74","volume":"39","author":"I Malavolta","year":"2013","unstructured":"Malavolta, I., Lago, P., Muccini, H., Pelliccione, P., Tang, A.: What industry needs from architectural languages: a survey. IEEE Trans. Softw. Eng. 39(6), 869\u2013891 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"6_CR25","doi-asserted-by":"publisher","unstructured":"Moln\u00e1r, V., Graics, B., V\u00f6r\u00f6s, A., Majzik, I., Varr\u00f3, D.: The gamma statechart composition framework: Design, verification and code generation for component-based reactive systems. In: Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings, ICSE 2018, pp. 113\u2013116. Association for Computing Machinery, New York (2018). https:\/\/doi.org\/10.1145\/3183440.3183489","DOI":"10.1145\/3183440.3183489"},{"key":"6_CR26","unstructured":"Object Management Group (OMG): UML Resource Page. https:\/\/www.omg.org\/spec\/UML\/. Accessed 12 June 2024"},{"key":"6_CR27","unstructured":"Object Management Group (OMG): Semantics of a Foundational Subset for Executable UML Models, Version 1.3. OMG Document Number formal\/17-07-02 (2017). https:\/\/www.omg.org\/spec\/FUML\/1.3\/"},{"key":"6_CR28","unstructured":"Object Management Group (OMG): Precise Semantics of UML Composite Structures, Specification v1.2. OMG Document Number: formal\/19-05-01 (2019). https:\/\/www.omg.org\/spec\/PSCS\/1.2\/"},{"key":"6_CR29","unstructured":"Object Management Group (OMG): Precise Semantics of UML State Machines, Specification v1.0. OMG Document Number: formal\/19-05-01 (2019). https:\/\/www.omg.org\/spec\/PSSM\/1.0\/"},{"key":"6_CR30","unstructured":"Roscoe, A.: The Theory and Practice of Concurrency. Prentice Hall (1997)"},{"key":"6_CR31","unstructured":"Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Pearson Higher Education (2004)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-78116-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T09:04:10Z","timestamp":1732784650000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-78116-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,29]]},"ISBN":["9783031781155","9783031781162"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-78116-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,29]]},"assertion":[{"value":"29 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"SBMF","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazilian Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Vit\u00f3ria","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 December 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 December 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sbmf2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}