{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T05:03:23Z","timestamp":1764306203505,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"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_5","type":"book-chapter","created":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T07:30:44Z","timestamp":1732779044000},"page":"68-85","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verifying Integrated Designs of UML State Machines and Activities Using CSP"],"prefix":"10.1007","author":[{"given":"Diego","family":"Ferreira","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lucas","family":"Lima","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,29]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Abdelhalim, I., et\u00a0al.: Formal verification of Tokeneer behaviours modelled in fUML using CSP|. In: Proceedings of the 12th International Conference on Formal Engineering Methods and Software Engineering, pp. 371\u2013387. ICFEM\u201910, Springer-Verlag, Berlin, Heidelberg (2010). http:\/\/dl.acm.org\/citation.cfm?id=1939864.1939895","DOI":"10.1007\/978-3-642-16901-4_25"},{"key":"5_CR2","unstructured":"Beck: Test Driven Development: By Example. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA (2002)"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"B\u00f6rger, E., St\u00e4rk, R.: Abstract State Machines. A Method for High-Level System Design and Analysis (2003). https:\/\/doi.org\/10.1007\/978-3-642-18216-7","DOI":"10.1007\/978-3-642-18216-7"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Elmansouri, R., Meghzili, S., Chaoui, A.: A UML 2.0 activity diagrams\/CSP integrated approach for modeling and verification of software systems. Comput. Sci. 22, (2021). https:\/\/doi.org\/10.7494\/csci.2021.22.2.3478","DOI":"10.7494\/csci.2021.22.2.3478"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Ferreira, D., Lima, L.: A CSP semantics for UML state machines aiming at hidden formal methods verification. In: Formal Methods: Foundations and Applications - 27th Brazilian Symposium, SBMF 2024, Vit\u00f3ria, Brazil, December 04\u201306, 2024, Proceedings. Lecture Notes in Computer Science (2024)","DOI":"10.1007\/978-3-031-78116-2_4"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.: Fdr3\u2014a modern refinement checker for csp. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol.\u00a08413, pp. 187\u2013201. Springer Berlin Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Graics, B., Moln\u00e1r, V., V\u00f6r\u00f6s, A., Majzik, I., Varro, D.: Mixed-semantics composition of statecharts for the component-based design of reactive systems. Softw. Syst. Model. 19, (2020). https:\/\/doi.org\/10.1007\/s10270-020-00806-5","DOI":"10.1007\/s10270-020-00806-5"},{"key":"5_CR8","doi-asserted-by":"publisher","first-page":"1723","DOI":"10.1002\/j.2334-5837.2004.tb00608.x","volume":"14","author":"B Haskins","year":"2004","unstructured":"Haskins, B., Stecklein, J., Dick, B., Moroney, G., Lovell, R., Dabney, J.: 8.4.2 error cost escalation through the project life cycle. INCOSE Int. Symp. 14, 1723\u20131737 (2004). https:\/\/doi.org\/10.1002\/j.2334-5837.2004.tb00608.x","journal-title":"INCOSE Int. Symp."},{"key":"5_CR9","volume-title":"Communicating and Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating and Sequential Processes. Prentice Hall (1985)"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Horv\u00e1th, B., et al.: Model checking as a service: towards pragmatic hidden formal methods. In: Proceedings of the 23rd ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings. MODELS \u201920, Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3417990.3421407","DOI":"10.1145\/3417990.3421407"},{"key":"5_CR11","first-page":"19","volume-title":"Formal Techniques for Networked and Distributed Systems","author":"F Khendek","year":"2001","unstructured":"Khendek, F., Bourduas, S., Vincent, D.: Stepwise design with message sequence charts. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) Formal Techniques for Networked and Distributed Systems, pp. 19\u201334. Springer, Boston (2001)"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Kiniry, J.R., Zimmerman, D.M.: Secret ninja formal methods. In: Cu\u00e9llar, J., Maibaum, T.S.E., Sere, K. (eds.) FM 2008: Formal Methods, 15th International Symposium on Formal Methods, Turku, Finland, May 26\u201330, 2008, Proceedings. Lecture Notes in Computer Science, vol.\u00a05014, pp. 214\u2013228. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-68237-0_16","DOI":"10.1007\/978-3-540-68237-0_16"},{"key":"5_CR13","first-page":"206","volume-title":"Perspect. Syst. Inform.","author":"J Kohlmeyer","year":"2010","unstructured":"Kohlmeyer, J., Guttmann, W.: Unifying the semantics of UML 2 state, activity and interaction diagrams. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) Perspect. Syst. Inform., pp. 206\u2013217. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)"},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-41071-0_13","volume-title":"Formal Methods: Foundations and Applications","author":"L Lima","year":"2013","unstructured":"Lima, L., Didier, A., Corn\u00e9lio, M.: A formal semantics for SYSML activity diagrams. In: Iyoda, J., de Moura, L. (eds.) Formal Methods: Foundations and Applications, pp. 179\u2013194. Springer Berlin Heidelberg, Berlin, Heidelberg (2013)"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Lima, L., Iyoda, J., Sampaio, A.: Refinement verification of sequence diagrams using CSP. In: Ribeiro, L., Lecomte, T. (eds.) Formal Methods: Foundations and Applications - 19th Brazilian Symposium, SBMF 2016, Natal, Brazil, November 23\u201325, 2016, Proceedings. Lecture Notes in Computer Science, vol. 10090, pp. 235\u2013252 (2016). https:\/\/doi.org\/10.1007\/978-3-319-49815-7_14","DOI":"10.1007\/978-3-319-49815-7_14"},{"key":"5_CR16","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102497","volume":"197","author":"L Lima","year":"2020","unstructured":"Lima, L., Tavares, A., Nogueira, S.C.: A framework for verifying deadlock and nondeterminism in UML activity diagrams based on CSP. Sci. Comput. Program. 197, 102497 (2020). https:\/\/doi.org\/10.1016\/j.scico.2020.102497","journal-title":"Sci. Comput. Program."},{"issue":"5","key":"5_CR17","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., Cavalcanti, A., Timmis, J., Woodcock, J.: Robochart: modelling and verification of the functional behaviour of robotic applications. Softw. Syst. Model. 18(5), 3097\u20133149 (2019). https:\/\/doi.org\/10.1007\/s10270-018-00710-z","journal-title":"Softw. Syst. Model."},{"key":"5_CR18","unstructured":"Miyazawa, A., Ribeiro, P., Ye, K., Cavalcanti, A., Li, W., Woodcock, J., Timmis, J.: Robochart reference manual. Tech. rep. University of York (2017). https:\/\/robostar.cs.york.ac.uk\/publications\/techreports\/reports\/robochart-reference.pdf"},{"key":"5_CR19","unstructured":"Object Management Group: OMG Unified Modeling Language (OMG UML), superstructure, version 2.4.1. Tech. rep. OMG (2011)"},{"key":"5_CR20","unstructured":"Object Management Group: Semantics of a Foundational Subset for Executable UML Models (FUML). Tech. rep., Object Management Group (2013). OMG Document Number: formal\/2013-08-06"},{"key":"5_CR21","unstructured":"OpenMBEE: Open Model Based Engineering Environment. https:\/\/www.openmbee.org\/. Accessed on 2023 Dec 10"},{"key":"5_CR22","unstructured":"OpenMBEE: TMT-SysML-Model. https:\/\/github.com\/Open-MBEE\/TMT-SysML-Model. Accessed on 2023 Jan 16"},{"key":"5_CR23","unstructured":"Reggio, G., Leotta, M., Ricca, F., Clerissi, D.: What are the used UML diagrams? A preliminary survey. In: EESSMOD@MoDELS, vol.\u00a01078, pp. 3\u201312 (2013)"},{"key":"5_CR24","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-540-25959-6_40","volume-title":"Applications of Graph Transformations with Industrial Relevance","author":"A Rensink","year":"2004","unstructured":"Rensink, A.: The groove simulator: a tool for state space generation. In: Pfaltz, J.L., Nagl, M., B\u00f6hlen, B. (eds.) Applications of Graph Transformations with Industrial Relevance, pp. 479\u2013485. Springer Berlin Heidelberg, Berlin, Heidelberg (2004)"},{"key":"5_CR25","unstructured":"The Object Management Group: OMG Systems Modeling Language. Standard 1.7 beta, Object Management Group, Milford, MA, USA (2022). https:\/\/www.omg.org\/spec\/SysML\/1.7\/Beta1"},{"issue":"4","key":"5_CR26","first-page":"541","volume":"11","author":"W Visser","year":"2012","unstructured":"Visser, W., Dwyer, M., Whalen, M.: The hidden models of model checking. Softw. Syst. Model. 11(4), 541\u2013555 (2012)","journal-title":"Softw. Syst. Model."}],"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_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,2]],"date-time":"2024-12-02T05:09:11Z","timestamp":1733116151000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-78116-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,29]]},"ISBN":["9783031781155","9783031781162"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-78116-2_5","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":"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"}}]}}