{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T14:07:30Z","timestamp":1749564450669,"version":"3.37.3"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2023,10,4]],"date-time":"2023-10-04T00:00:00Z","timestamp":1696377600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,10,4]],"date-time":"2023-10-04T00:00:00Z","timestamp":1696377600000},"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":["Softw Syst Model"],"published-print":{"date-parts":[[2024,6]]},"DOI":"10.1007\/s10270-023-01127-z","type":"journal-article","created":{"date-parts":[[2023,10,4]],"date-time":"2023-10-04T16:01:31Z","timestamp":1696435291000},"page":"765-798","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A formal component model for UML based on CSP aiming at compositional verification"],"prefix":"10.1007","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0828-1412","authenticated-orcid":false,"given":"Fl\u00e1via","family":"Falc\u00e3o","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1859-8437","authenticated-orcid":false,"given":"Lucas","family":"Lima","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6593-577X","authenticated-orcid":false,"given":"Augusto","family":"Sampaio","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5627-0910","authenticated-orcid":false,"given":"Pedro","family":"Antonino","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,10,4]]},"reference":[{"key":"1127_CR1","volume-title":"The Unified Modeling Language User Guide","author":"G Booch","year":"2005","unstructured":"Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Addison-Wesley, Upper Saddle River (2005)"},{"issue":"6","key":"1127_CR2","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1007\/s00165-016-0375-1","volume":"28","author":"MVM Oliveira","year":"2016","unstructured":"Oliveira, M.V.M., et al.: Rigorous development of component-based systems using component metadata and patterns. Formal Aspects Comput. 28(6), 937\u20131004 (2016)","journal-title":"Formal Aspects Comput."},{"key":"1127_CR3","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"EM Clarke","year":"1996","unstructured":"Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. 28, 626\u2013643 (1996)","journal-title":"ACM Comput. Surv."},{"issue":"4","key":"1127_CR4","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1016\/j.scico.2008.08.003","volume":"74","author":"Z Chen","year":"2009","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)","journal-title":"Sci. Comput. Program."},{"issue":"5","key":"1127_CR5","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/s00446-012-0168-6","volume":"25","author":"B Bonakdarpour","year":"2012","unstructured":"Bonakdarpour, B., Bozga, M., Jaber, M., Quilbeuf, J., Sifakis, J.: A framework for automated distributed implementation of component-based models. Distrib. Comput. 25(5), 383\u2013409 (2012)","journal-title":"Distrib. Comput."},{"key":"1127_CR6","doi-asserted-by":"crossref","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in bip. In: Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods, pp. 3\u201312. IEEE Computer Society, Washington, DC, USA (2006)","DOI":"10.1109\/SEFM.2006.27"},{"key":"1127_CR7","doi-asserted-by":"crossref","unstructured":"Horv\u00e1th, B., Guerra, E., Iovino, L. et\u00a0al. : Model checking as a service: towards pragmatic hidden formal methods. In: Guerra, E., Iovino, L. (eds.) MODELS\u201920: ACM\/IEEE 23rd International Conference on Model Driven Engineering Languages and Systems. ACM (2020)","DOI":"10.1145\/3417990.3421407"},{"key":"1127_CR8","doi-asserted-by":"crossref","unstructured":"Object Management Group (OMG). OMG System Modeling Language (OMG SysML), Version 1.5. OMG Document Number formal\/17-05-01 (https:\/\/www.omg.org\/spec\/SysML\/1.5\/) (2017)","DOI":"10.1016\/B978-1-78548-171-0.50001-3"},{"key":"1127_CR9","unstructured":"Ramos, R.T.: Systematic Development of Trustworthy Component-based Systems. Ph.D. thesis, UFPE, Brazil (2011). https:\/\/repositorio.ufpe.br\/handle\/123456789\/2073"},{"key":"1127_CR10","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-05089-3_10","volume-title":"FM 2009: Formal Methods","author":"R Ramos","year":"2009","unstructured":"Ramos, R., Sampaio, A., Mota, A.: Systematic development of trustworthy component systems. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009: Formal Methods, pp. 140\u2013156. Springer Berlin Heidelberg, Berlin, Heidelberg (2009)"},{"key":"1127_CR11","volume-title":"The Theory and Practice of Concurrency","author":"AW Roscoe","year":"1997","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1997)"},{"key":"1127_CR12","doi-asserted-by":"crossref","unstructured":"Falc\u00e3o, F., Lima, L., Sampaio, A.: Safe and Constructive Design with UML Components: 21st Brazilian Symposium, SBMF 2018, Salvador, Brazil, November 26-30, 2018, Proceedings, pp. 234\u2013251. Springer (2018)","DOI":"10.1007\/978-3-030-03044-5_15"},{"key":"1127_CR13","unstructured":"Management\u00a0Group, O.: Omg unified modeling language \u2013 version 2.5.1. https:\/\/www.omg.org\/spec\/UML\/2.5.1 (2017). https:\/\/www.omg.org\/spec\/UML\/2.5.1"},{"key":"1127_CR14","unstructured":"Vision, C.: Astah - premier diagramming, modeling software & tools (2022). https:\/\/astah.net\/"},{"volume-title":"Component-Based Software Engineering: Putting the Pieces Together","year":"2001","key":"1127_CR15","unstructured":"Heineman, G.T., Councill, W.T. (eds.): Component-Based Software Engineering: Putting the Pieces Together. Addison-Wesley Longman Publishing Co., Boston (2001)"},{"key":"1127_CR16","unstructured":"Lau, K.-K., Wang, Z.: A survey of software component models. Tech. Rep., in Software Engineering and Advanced Applications. 31st EUROMICRO Conference: IEEE Computer Society (2005)"},{"key":"1127_CR17","unstructured":"Object Management Group (OMG): UML Profile for MARTE: Modeling and Analysis of Real-Time Embedded Systems. OMG Document Number: formal\/19-04-01 (https:\/\/www.omg.org\/spec\/MARTE\/1.2) (2019)"},{"key":"1127_CR18","doi-asserted-by":"crossref","unstructured":"Selic, B.: A systematic approach to domain-specific language design using uml. In: 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC\u201907), pp. 2\u20139 (2007)","DOI":"10.1109\/ISORC.2007.10"},{"key":"1127_CR19","unstructured":"Object Management Group (OMG): Object Constraint Language - Spec v2.4. OMG Document Number: formal\/2014-02-03 (https:\/\/www.omg.org\/spec\/OCL\/2.4\/) (2014)"},{"key":"1127_CR20","unstructured":"Object Management Group (OMG): Semantics of a Foundational Subset for Executable UML Models, Version 1.3. OMG Document Number formal\/formal\/17-07-02 (https:\/\/www.omg.org\/spec\/FUML\/1.3\/) (2017)"},{"key":"1127_CR21","unstructured":"Object Management Group (OMG): Precise Semantics of UML State Machines - Specification v1.0. OMG Document Number: formal\/19-05-01 (https:\/\/www.omg.org\/spec\/PSSM\/1.0\/) (2019)"},{"key":"1127_CR22","unstructured":"Object Management Group (OMG): Precise Semantics of UML Composite Structures - Specification v1.2. OMG Document Number: formal\/19-05-01 (https:\/\/www.omg.org\/spec\/PSCS\/1.2\/) (2019)"},{"key":"1127_CR23","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.: Fdr3: A modern refinement checker for csp. In: Abraham, E. & Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, vol. 8413 of Lecture Notes in Computer Science, pp. 187\u2013201. Springer Berlin Heidelberg (2014)","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"1127_CR24","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/978-3-319-11737-9_2","volume-title":"Formal Methods and Software Engineering","author":"A Boulgakov","year":"2014","unstructured":"Boulgakov, A., Gibson-Robinson, T., Roscoe, A.W., Merz, S., Pang, J.: Computing maximal bisimulations. In: Merz, S., Pang, J. (eds.) Formal Methods and Software Engineering, pp. 11\u201326. Springer, Cham (2014)"},{"issue":"4","key":"1127_CR25","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1002\/stvr.1498","volume":"24","author":"A Sampaio","year":"2013","unstructured":"Sampaio, A., Nogueira, S., Mota, A., Isobe, Y.: Sound and mechanised compositional verification of input\u2013output conformance. Softw. Test. Verif. Reliab. 24(4), 289\u2013319 (2013)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"1127_CR26","unstructured":"Company, B.: B &o softwares (2022). http:\/\/www.bang-olufsen.com\/"},{"key":"1127_CR27","unstructured":"Martin, J.M.R.: The Design and Construction of Deadlock-Free Concurrent Systems. Ph.D. thesis, University of Buckingham (1996)"},{"key":"1127_CR28","doi-asserted-by":"crossref","unstructured":"Antonino, P.R.G., Sampaio, A., Woodcock, J.: A refinement based strategy for local deadlock analysis of networks of CSP processes. In: FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, Vol. 8442 of Lecture Notes in Computer Science, pp. 62\u201377. Springer (2014)","DOI":"10.1007\/978-3-319-06410-9_5"},{"key":"1127_CR29","doi-asserted-by":"crossref","unstructured":"Antonino, P.R., Oliveira, M.M., Sampaio, A.C., Kristensen, K.E., Bryans, J.W.: Leadership election: \u017aan industrial sos application of compositional deadlock verification. In: Proceedings of the 6th International Symposium on NASA Formal Methods - vol. 8430. Springer, Berlin, Heidelberg (2014)","DOI":"10.1007\/978-3-319-06200-6_3"},{"key":"1127_CR30","doi-asserted-by":"publisher","unstructured":"Antonino, P., Sampaio, A., Woodcock, J.: A pattern-based deadlock-freedom analysis strategy for concurrent systems. CoRR abs\/2207.08854 (2022). https:\/\/doi.org\/10.48550\/ARXIV.2207.08854","DOI":"10.48550\/ARXIV.2207.08854"},{"key":"1127_CR31","first-page":"63","volume":"24","author":"M Gr\u00fcninger","year":"2003","unstructured":"Gr\u00fcninger, M., Menzel, C.: The process specification language (psl) theory and applications. AI Mag. 24, 63\u201374 (2003)","journal-title":"AI Mag."},{"key":"1127_CR32","doi-asserted-by":"crossref","unstructured":"Chen, Z., Morisset, C., Stolz, V.: Specification and validation of behavioural protocols in the rcos modeler. In: Arbab, F. (ed.) Proceedings of the Third IPM International Conference on Fundamentals of Software Engineering, FSEN\u201909, pp. 387\u2013401. Springer, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-11623-0_23"},{"key":"1127_CR33","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-030-90636-8_2","volume-title":"Formal Aspects of Component Software","author":"S Chehida","year":"2021","unstructured":"Chehida, S., Baouya, A., Bensalem, S.: Component-based approach combining uml and bip for rigorous system design. In: Sala\u00fcn, G., Wijs, A. (eds.) Formal Aspects of Component Software, pp. 27\u201343. Springer, Cham (2021)"},{"key":"1127_CR34","doi-asserted-by":"publisher","first-page":"1","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, 1\u201335 (2020)","journal-title":"Softw. Syst. Model."},{"key":"1127_CR35","doi-asserted-by":"crossref","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 Proceedings, ICSE \u201918, pp. 113\u2013116. Association for Computing Machinery, New York, NY, USA (2018)","DOI":"10.1145\/3183440.3183489"},{"key":"1127_CR36","volume-title":"Real-Time Object-Oriented Modeling","author":"B Selic","year":"1994","unstructured":"Selic, B., Gullekson, G., Ward, P.T.: Real-Time Object-Oriented Modeling. Wiley, New York (1994)"},{"key":"1127_CR37","unstructured":"Pereira, D.I.A., Oliveira, M.V.M., Silva, S.R.R.: Tool support for formal component-based development. Tech. Rep., Escola de Inform\u00e1tica Te\u00f3rica e M\u00e9todos Formais (ETMF 2016) (2016)"},{"issue":"3","key":"1127_CR38","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)","journal-title":"Softw. Syst. Model."},{"key":"1127_CR39","doi-asserted-by":"crossref","unstructured":"Gibson, C., Karban, R., Andolfato, L., Day, J.: Abstractions for executable and checkable fault management models. Procedia Comput. Sci. 28, 146\u2013154 (2014). Conference on Systems Engineering Research","DOI":"10.1016\/j.procs.2014.03.019"},{"key":"1127_CR40","first-page":"1","volume-title":"Software Language Engineering","author":"B Meyers","year":"2014","unstructured":"Meyers, B., et al.: Promobox: a framework for generating domain-specific property languages. In: Combemale, B., Pearce, D.J., Barais, O., Vinju, J.J. (eds.) Software Language Engineering, pp. 1\u201320. Springer, Cham (2014)"},{"key":"1127_CR41","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/11494881_7","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"R Ramos","year":"2005","unstructured":"Ramos, R., Sampaio, A., Mota, A.: A semantics for uml-rt active classes via mapping into circus. In: Steffen, M., Zavattaro, G. (eds.) Formal Methods for Open Object-Based Distributed Systems, pp. 99\u2013114. Springer Berlin Heidelberg, Berlin, Heidelberg (2005)"},{"key":"1127_CR42","doi-asserted-by":"crossref","unstructured":"Woodcock, J. et\u00a0al.: Features of cml: A formal modelling language for systems of systems. In: 2012 7th International Conference on System of Systems Engineering (SoSE), pp. 1\u20136 (2012)","DOI":"10.1109\/SYSoSE.2012.6384144"},{"key":"1127_CR43","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511626975","volume-title":"Modelling Systems: Practical Tools and Techniques in Software Development","author":"J Fitzgerald","year":"2009","unstructured":"Fitzgerald, J., Larsen, P.G.: Modelling Systems: Practical Tools and Techniques in Software Development. Cambridge University Press, New York (2009)"},{"key":"1127_CR44","doi-asserted-by":"crossref","unstructured":"Cavalcanti, A., et\u00a0al.: Modelling and verification for swarm robotics. In: Furia, C.A., Winter, K. (eds.) Integrated Formal Methods\u201414th International Conference, IFM 2018, vol. 11023, pp. 1\u201319 (2018)","DOI":"10.1007\/978-3-319-98938-9_1"},{"key":"1127_CR45","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.ipl.2017.12.011","volume":"133","author":"M Conserva Filho","year":"2018","unstructured":"Conserva Filho, M., Oliveira, M., Sampaio, A., Cavalcanti, A.: Compositional and local livelock analysis for csp. Inf. Process. Lett. 133, 21\u201325 (2018)","journal-title":"Inf. Process. Lett."},{"key":"1127_CR46","doi-asserted-by":"crossref","unstructured":"Otoni, R., Cavalcanti, A., Sampaio, A.: Local analysis of determinism for CSP. In: da\u00a0Costa\u00a0Cavalheiro, S.A., Fiadeiro, J.L. (eds.) Formal Methods: Foundations and Applications - 20th Brazilian Symposium, SBMF 2017, vol. 10623 of Lecture Notes in Computer Science, pp. 107\u2013124. Springer (2017)","DOI":"10.1007\/978-3-319-70848-5_8"},{"key":"1127_CR47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21491-7","volume-title":"Introduction to Concurrency Theory: Transition Systems and CCS","author":"R Gorrieri","year":"2015","unstructured":"Gorrieri, R., Versari, C.: Introduction to Concurrency Theory: Transition Systems and CCS, 1st edn. Springer, Cham (2015)","edition":"1"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-023-01127-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-023-01127-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-023-01127-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T01:04:02Z","timestamp":1730250242000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-023-01127-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,4]]},"references-count":47,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["1127"],"URL":"https:\/\/doi.org\/10.1007\/s10270-023-01127-z","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2023,10,4]]},"assertion":[{"value":"4 March 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 March 2023","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 August 2023","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 October 2023","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}