{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T05:03:13Z","timestamp":1764306193935,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"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_4","type":"book-chapter","created":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T07:31:05Z","timestamp":1732779065000},"page":"49-67","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A CSP Semantics for UML State Machines Aiming at Hidden Formal Methods Verification"],"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":[{"issue":"1","key":"4_CR1","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","volume":"14","author":"T Bolognesi","year":"1987","unstructured":"Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Comput. Netw. ISDN Syst. 14(1), 25\u201359 (1987)","journal-title":"Comput. Netw. ISDN Syst."},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"B\u00f6rger, E., Cavarra, A., Riccobene, E.: Modeling the meaning of transitions from and to concurrent states in uml state machines. In: Proceedings of the 2003 ACM Symposium on Applied Computing, pp. 1086\u20131091. SAC \u201903, Association for Computing Machinery, New York, NY, USA (2003). https:\/\/doi.org\/10.1145\/952532.952745","DOI":"10.1145\/952532.952745"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines: A Method for High-level System Design and Analysis; with 19 Tables. Springer (2003)","DOI":"10.1007\/978-3-642-18216-7"},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1007\/978-3-319-24770-0_47","volume-title":"Information and Software Technologies","author":"S Djaaboub","year":"2015","unstructured":"Djaaboub, S., Kerkouche, E., Chaoui, A.: From UML statecharts to LOTOS expressions using graph transformation. In: Dregvaite, G., Damasevicius, R. (eds.) Information and Software Technologies, pp. 548\u2013559. Springer International Publishing, Cham (2015)"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.: Fdr3 -a modern refinement checker for csp. In: \u00c0brah\u00e0m, 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":"4_CR6","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. Soft. Syst. Model. 19, (2020). https:\/\/doi.org\/10.1007\/s10270-020-00806-5","DOI":"10.1007\/s10270-020-00806-5"},{"key":"4_CR7","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":"4_CR8","volume-title":"Communicating and Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating and Sequential Processes. Prentice Hall (1985)"},{"key":"4_CR9","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":"4_CR10","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":"4_CR11","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-30, 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"},{"issue":"5","key":"4_CR12","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":"4_CR13","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":"4_CR14","doi-asserted-by":"publisher","unstructured":"Ng, M.Y., Butler, M.: Towards formalizing UML state diagrams in CSP. In: First International Conference onSoftware Engineering and Formal Methods, 2003, Proceedings, pp. 138\u2013147 (2003). https:\/\/doi.org\/10.1109\/SEFM.2003.1236215","DOI":"10.1109\/SEFM.2003.1236215"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Object Management Group: OMG Unified Modeling Language (OMG UML), version 2.5.1. Tech. rep. OMG (2017)","DOI":"10.1016\/B978-1-78548-171-0.50001-3"},{"key":"4_CR16","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":"4_CR17","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: Pat: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, pp. 709\u2013714. Springer Berlin Heidelberg, Berlin, Heidelberg (2009)"},{"key":"4_CR18","unstructured":"Syriani, E., Vangheluwe, H., Mannadiar, R., Hansen, C., Van\u00a0Mierlo, S., Ergin, H.: Atompm: a web-based modeling environment. In: Joint proceedings of MODELS\u201913 Invited Talks, Demonstration Session, Poster Session, and ACM Student Research Competition co-located with the 16th International Conference on Model Driven Engineering Languages and Systems (MODELS 2013): September 29-October 4, 2013, Miami, USA, pp. 21\u201325 (2013)"},{"key":"4_CR19","unstructured":"Vision, C.: Astah (2019). http:\/\/astah.net\/"},{"issue":"4","key":"4_CR20","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."},{"key":"4_CR21","doi-asserted-by":"publisher","unstructured":"Zhang, S., Liu, Y.: An automatic approach to model checking UML state machines. In: IEEE International Conference on Secure Software Integration and Reliability Improvement Companion, pp. 1\u20136 (06 2010). https:\/\/doi.org\/10.1109\/SSIRI-C.2010.11","DOI":"10.1109\/SSIRI-C.2010.11"}],"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_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T09:04:04Z","timestamp":1732784644000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-78116-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,29]]},"ISBN":["9783031781155","9783031781162"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-78116-2_4","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"}}]}}