{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,20]],"date-time":"2026-08-20T15:04:06Z","timestamp":1787238246050,"version":"3.56.0"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2015,9,1]],"date-time":"2015-09-01T00:00:00Z","timestamp":1441065600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"EU Horizon 2020 INTO-CPS"},{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["287829"],"award-info":[{"award-number":["287829"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003593","name":"Conselho Nacional de Desenvolvimento Cient\u00edfico e Tecnol\u00f3gico","doi-asserted-by":"publisher","award":["483329\/2012-6"],"award-info":[{"award-number":["483329\/2012-6"]}],"id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2017,7]]},"DOI":"10.1007\/s10270-015-0492-y","type":"journal-article","created":{"date-parts":[[2015,8,31]],"date-time":"2015-08-31T03:24:31Z","timestamp":1440991471000},"page":"875-902","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["An integrated semantics for reasoning about SysML design models using refinement"],"prefix":"10.1007","volume":"16","author":[{"given":"Lucas","family":"Lima","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alvaro","family":"Miyazawa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"M\u00e1rcio","family":"Corn\u00e9lio","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Juliano","family":"Iyoda","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Augusto","family":"Sampaio","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ralph","family":"Hains","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Adrian","family":"Larkham","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vaughan","family":"Lewis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,9,1]]},"reference":[{"key":"492_CR1","unstructured":"OMG, OMG Systems Modeling Language (OMG SysML), Version 1.3 (2012)"},{"key":"492_CR2","doi-asserted-by":"crossref","DOI":"10.1049\/PBPC007E","volume-title":"SysML for Systems Engineering","author":"J Holt","year":"2008","unstructured":"Holt, J., Perry, S.: SysML for Systems Engineering. IET, London (2008)"},{"key":"492_CR3","volume-title":"A Practical Guide to SysML: The Systems Modeling Language","author":"S Friedenthal","year":"2011","unstructured":"Friedenthal, S., Moore, A., Steiner, R.: A Practical Guide to SysML: The Systems Modeling Language, 2nd edn. Morgan Kaufmann, San Francisco (2011)","edition":"2"},{"key":"492_CR4","unstructured":"Rational Rhapsody Architect for Systems Engineers. http:\/\/www-142.ibm.com\/software\/products\/us\/en\/ratirhaparchforsystengi (2013)"},{"key":"492_CR5","unstructured":"Artisan Studio. http:\/\/atego.com\/products\/artisan-studio\/ (2013)"},{"key":"492_CR6","unstructured":"Sparx Systems\u2019 Enterprise Architect supports the Systems Modeling Language. http:\/\/sparxsystems.com\/products\/mdg\/tech\/sysml\/ (2013)"},{"key":"492_CR7","doi-asserted-by":"crossref","unstructured":"Woodcock, J., Cavalcanti, A., Fitzgerald, J., Larsen, P., Miyazawa, A., Perry, S.: Features of CML: a formal modelling language for systems of systems. In: 7th International Conference on System of Systems Engineering, pp.\u00a01\u20136 (2012)","DOI":"10.1109\/SYSoSE.2012.6384144"},{"key":"492_CR8","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/s10472-011-9267-5","volume":"63","author":"H Graves","year":"2011","unstructured":"Graves, H., Bijan, Y.: Using formal methods with SysML in aerospace design and engineering. Ann. Math. Artif. Intell. 63, 53\u2013102 (2011)","journal-title":"Ann. Math. Artif. Intell."},{"key":"492_CR9","doi-asserted-by":"crossref","unstructured":"Ramos, R., Sampaio, A., Mota, A.: A semantics for UML-RT active classes via mapping into circus. In: Steffen, M., Zavattaro, G. (eds.) FMOODS. Lecture Notes in Computer Science, vol.\u00a03535. Springer, pp.\u00a099\u2013114 (2005)","DOI":"10.1007\/11494881_7"},{"key":"492_CR10","unstructured":"Storrle, H.: Trace semantics of interactions in uml 2.0 abstract (2004)"},{"key":"492_CR11","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, ICFEM\u201910. Springer, Berlin, Heidelberg, pp.\u00a0371\u2013387 (2010)","DOI":"10.1007\/978-3-642-16901-4_25"},{"issue":"2\u20133","key":"492_CR12","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/s00165-003-0008-3","volume":"15","author":"J Davies","year":"2003","unstructured":"Davies, J., Crichton, C.: Concurrency and refinement in the unified modeling language. Form. Aspects Comput. 15(2\u20133), 118\u2013145 (2003)","journal-title":"Form. Aspects Comput."},{"key":"492_CR13","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":"492_CR14","unstructured":"Object Management Group, Precise Semantics Of UML Composite Structures (PSCS). Tech. rep., Object Management Group, 2014. OMG Document Number: 1.0 - Beta 1"},{"key":"492_CR15","doi-asserted-by":"crossref","unstructured":"Abdelhalim, I., Schneider, S., Treharne, H.: An optimization approach for effective formalized fuml model checking. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM. Lecture Notes in Computer Science, vol.\u00a07504. Springer, pp.\u00a0248\u2013262 (2012)","DOI":"10.1007\/978-3-642-33826-7_17"},{"key":"492_CR16","doi-asserted-by":"crossref","unstructured":"Laurent, Y., Bendraou, R., Baarir, S., Gervais, M.-P.: Formalization of fuml: An application to process verification. In: Jarke, M., Mylopoulos, J., Quix, C., Rolland, C., Manolopoulos, Y., Mouratidis, H., Horkoff, J. (eds.) Advanced Information Systems Engineering. Lecture Notes in Computer Science, vol.\u00a08484. Springer International Publishing, pp.\u00a0347\u2013363 (2014)","DOI":"10.1007\/978-3-319-07881-6_24"},{"key":"492_CR17","doi-asserted-by":"crossref","unstructured":"Miyazawa, A., Lima, L., Cavalcanti, A.: Formal models of sysml blocks. In: Groves, L., Sun, J. (eds.) Formal Methods and Software Engineering. Lecture Notes in Computer Science, vol.\u00a08144. Springer, Berlin, Heidelberg (2013)","DOI":"10.1007\/978-3-642-41202-8_17"},{"key":"492_CR18","doi-asserted-by":"crossref","unstructured":"Lima, L., Didier, A., Corn\u00e9lio, M.: A formal semantics for sysml activity diagrams. In: Iyoda, J., Moura, L. (eds.) Formal Methods: Foundations and Applications. Lecture Notes in Computer Science, vol.\u00a08195. Springer, Berlin, Heidelberg, pp.\u00a0179\u2013194 (2013)","DOI":"10.1007\/978-3-642-41071-0_13"},{"key":"492_CR19","unstructured":"Lima, L., Iyoda, J., Sampaio, A.: A formal semantics for sequence diagrams and a strategy for system analysis. In: Proceedings of the International Conference on Model-Driven Engineering and Software Development (MODELSWARD) (2014)"},{"key":"492_CR20","unstructured":"Object Management Group, OMG Unified Modeling Language (OMG UML), superstructure, version 2.3. Tech. rep., OMG (2010)"},{"key":"492_CR21","unstructured":"OMG, OMG Unified Modeling Language (OMG UML), superstructure, version 2.4.1. Tech. rep., Object Management Group (2011)"},{"key":"492_CR22","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511626975","volume-title":"Modelling Systems\u2014Practical Tools and Techniques in Software Development","author":"J Fitzgerald","year":"2009","unstructured":"Fitzgerald, J., Larsen, P.G.: Modelling Systems\u2014Practical Tools and Techniques in Software Development, 2nd edn. Cambridge University Press, Cambridge (2009)","edition":"2"},{"key":"492_CR23","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"492_CR24","doi-asserted-by":"crossref","unstructured":"Woodcock, J., Cavalcanti, A., Coleman, J., Didier, A., Larsen, P.G., Miyazawa, A., Oliveira, M.: CML Definition 0. Tech. Rep. D23.1, COMPASS (2012)","DOI":"10.1109\/SYSoSE.2012.6384144"},{"key":"492_CR25","unstructured":"Miyazawa, A., Albertins, L., Iyoda, J., Corn\u00e9lio, M., Payne, R., Cavalcanti, A.: Final report on combining SysML and CML. Tech. rep., COMPASS (2013)"},{"key":"492_CR26","unstructured":"Lima, L., Miyazawa, A., Cavalcanti, A.: Case Studies of SysML to CML transformations. Tech. rep., University of York. http:\/\/www.compass-research.eu\/whitepapers.html (2014)"},{"key":"492_CR27","doi-asserted-by":"crossref","unstructured":"Miyazawa, A., Cavalcanti, A.: Formal refinement in SysML. In: Proceedings of the 11th International Conference on Integrated Formal Methods. Accepted for publication (2014)","DOI":"10.1007\/978-3-319-10181-1_10"},{"key":"492_CR28","doi-asserted-by":"crossref","unstructured":"Coleman, J., Malmos, A., Larsen, P., Peleska, J., Hains, R., Andrews, Z., Payne, R., Foster, S., Miyazawa, A., Bertolini, C., Didier, A.: COMPASS tool vision for a system of systems collaborative development environment. In: 7th International Conference on System of Systems Engineering, pp.\u00a0451\u2013456 (2012)","DOI":"10.1109\/SYSoSE.2012.6384150"},{"key":"492_CR29","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.: Fdr3\u2014a modern refinement checker for csp. In: Abraham, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol.\u00a08413. Springer, Berlin, Heidelberg, pp.\u00a0187\u2013201 (2014)","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"492_CR30","unstructured":"Lima, L.: Report on Guidelines for Analysis of SysML Diagrams. Tech. rep., University of York. http:\/\/www.compass-research.eu\/Project\/Publications\/SysML2CML\/reportYork2014.pdf (2014)"},{"key":"492_CR31","doi-asserted-by":"crossref","unstructured":"Breu, R., Grosu, R., Huber, F., Rumpe, B., Schwerin, W.: Systems, views and models of UML. In: UML Workshop, pp.\u00a093\u2013108 (1997)","DOI":"10.1007\/978-3-642-48673-9_7"},{"key":"492_CR32","doi-asserted-by":"crossref","unstructured":"Lano, K., Evans, A.: Rigorous development in UML. In: Proceedings of the Fundamental Approaches to Software Engineering (FASE), pp.\u00a0129\u2013144 (1999)","DOI":"10.1007\/978-3-540-49020-3_9"},{"key":"492_CR33","doi-asserted-by":"crossref","unstructured":"Kuske, S., Gogolla, M., Kollmann, R., Kreowski, H.-J.: An integrated semantics for uml class, object and state diagrams based on graph transformation. In: Butler, M., Petre, L., Sere, K. (eds.) Integrated Formal Methods. Lecture Notes in Computer Science, vol.\u00a02335. Springer, Berlin, Heidelberg, pp.\u00a011\u201328 (2002)","DOI":"10.1007\/3-540-47884-1_2"},{"key":"492_CR34","doi-asserted-by":"crossref","unstructured":"Rasch, H., Wehrheim, H.: Checking consistency in UML diagramms: classes and state machines. In: Najm, E., Nestmann, U., Stevens, P. (eds.) Formal Methods for Open Object-Based Distributed Systems (6th FMOODS\u201903). Lecture Notes in Computer Science (LNCS), Paris, France, vol.\u00a02884. Springer, Berlin\/New York, pp.\u00a0229\u2013243, Nov. 2003","DOI":"10.1007\/978-3-540-39958-2_16"},{"key":"492_CR35","unstructured":"Hamilton, M.H., Hackler, W.R., Margaret, C., Hamilton, H., Published, W.R.H., Permission, U.I.: A formal universal systems semantics for SysML (2007)"},{"issue":"1","key":"492_CR36","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/s10472-011-9267-5","volume":"63","author":"H Graves","year":"2011","unstructured":"Graves, H., Bijan, Y.: Using formal methods with SysML in aerospace design and engineering. Ann. Math. Artif. Intell. 63(1), 53\u2013102 (2011)","journal-title":"Ann. Math. Artif. Intell."},{"key":"492_CR37","doi-asserted-by":"crossref","unstructured":"Graves, H.: Integrating reasoning with SysML. In: INCOSE Symposium, Rome, Italy (2012)","DOI":"10.1002\/j.2334-5837.2012.tb01470.x"},{"key":"492_CR38","unstructured":"Graves, H.: Modeling structure in description logic. In: Proceedings of the International Workshop on Description Logics (DL2011), Barcelona, Spain (2011)"},{"key":"492_CR39","unstructured":"Caf\u00e9, D.C., Boulanger, F., Jacquet, C., Hardebolle, C., Santos, F.V.D.: Multi-paradigm semantics for simulating SysML models using SystemC-AMS. In: Proceedings of the Forum on Specification & Design Languages, Sept 2013"},{"key":"492_CR40","unstructured":"Broy, M., Cengarle, M.V., Rumpe, B.: Semantics of UML\u2014Towards a System Model for UML: The Structural Data Model. Tech. Rep. TUM-I0612, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Feb 2006"},{"key":"492_CR41","unstructured":"Broy, M., Cengarle, M.V., Rumpe, B.: Semantics of UML\u2014Towards a System Model for UML: The Control Model. Tech. Rep. TUM-I0710, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Feb 2007"},{"key":"492_CR42","unstructured":"Broy, M., Cengarle, M.V., Rumpe, B.: Semantics of UML\u2014Towards a System Model for UML: The State Machine Model. Tech. Rep. TUM-I0711, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Feb 2007"},{"key":"492_CR43","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-5265-9","volume-title":"The Object-Z Specification Language","author":"G Smith","year":"2000","unstructured":"Smith, G.: The Object-Z Specification Language. Kluwer, Dordrecht (2000)"},{"issue":"1\u20132","key":"492_CR44","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1016\/j.artint.2005.05.003","volume":"168","author":"D Berardi","year":"2005","unstructured":"Berardi, D., Calvanese, D., Giacomo, G.D.: Reasoning on UML class diagrams. Artif. Intell. 168(1\u20132), 70\u2013118 (2005)","journal-title":"Artif. Intell."},{"key":"492_CR45","doi-asserted-by":"crossref","unstructured":"Vachoux, A., Grimm, C., Einwich, K.: Analog and mixed signal modelling with SystemC-AMS. In: ISCAS (3), pp. 914\u2013917 (2003)","DOI":"10.1109\/ISCAS.2003.1205169"},{"key":"492_CR46","doi-asserted-by":"crossref","unstructured":"Panda, P.R.: SystemC. In: ISSS, pp.\u00a075\u201380 (2001)","DOI":"10.1145\/500001.500018"},{"issue":"3","key":"492_CR47","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(3), 63\u201374 (2003)","journal-title":"AI Mag."},{"key":"492_CR48","unstructured":"Lilius, J., Paltor, I.P.: The semantics of UML State Machines. Tech. rep., Turku Centre for Computer Science (1999)"},{"key":"492_CR49","unstructured":"Meng, S., Naixiao, Z., Barbosa, L.S.: On the semantics and refinement of uml statecharts: a coalgebraic view. In: Proceedings of the 2nd International Conference on Software Engineering and Formal Methods, IEEE Computer Society (2004)"},{"key":"492_CR50","doi-asserted-by":"crossref","unstructured":"Eichner, C., Fleischhack, H., Meyer, R., Schrimpf, U., Stehno, C.: Compositional semantics for UML 2.0 sequence diagrams using Petri Nets. In: SDL Forum. LNCS, vol.\u00a03530. Springer, pp.\u00a0133\u2013148 (2005)","DOI":"10.1007\/11506843_9"},{"key":"492_CR51","volume-title":"Unifying Theories of Programming","author":"CAR Hoare","year":"1998","unstructured":"Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Upper Saddle River (1998)"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-015-0492-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-015-0492-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-015-0492-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-015-0492-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T05:22:27Z","timestamp":1748582547000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-015-0492-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,1]]},"references-count":51,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,7]]}},"alternative-id":["492"],"URL":"https:\/\/doi.org\/10.1007\/s10270-015-0492-y","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9,1]]}}}