{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T16:43:49Z","timestamp":1761324229241},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2019,7,13]],"date-time":"2019-07-13T00:00:00Z","timestamp":1562976000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,7,13]],"date-time":"2019-07-13T00:00:00Z","timestamp":1562976000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Soft Comput"],"published-print":{"date-parts":[[2020,3]]},"DOI":"10.1007\/s00500-019-04181-2","type":"journal-article","created":{"date-parts":[[2019,7,13]],"date-time":"2019-07-13T04:54:08Z","timestamp":1562993648000},"page":"4149-4164","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Formalizing UML\/OCL structural features with FoCaLiZe"],"prefix":"10.1007","volume":"24","author":[{"given":"Messaoud","family":"Abbas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Choukri-Bey","family":"Ben-Yelles","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Renaud","family":"Rioboo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,7,13]]},"reference":[{"key":"4181_CR1","unstructured":"Abbas M (2014) Using FoCaLiZe to check OCL constraints on UML classes. In: International conference on information technology for organization development, IT4OD 2014, conference proceedings, pp 31\u201338"},{"key":"4181_CR2","doi-asserted-by":"crossref","unstructured":"Abbas M, Ben-Yelles CB, Rioboo R (2014) Modeling UML template classes with FoCaLiZe. In: The international conference on integrated formal methods, IFM2014, LNCS, vol 8739. Springer, pp 87\u2013102","DOI":"10.1007\/978-3-319-10181-1_6"},{"issue":"1","key":"4181_CR3","first-page":"34","volume":"13","author":"M Abbas","year":"2018","unstructured":"Abbas M, Ben-Yelles CB, Rioboo R (2018) Modelling UML state machines with FoCaLiZe. Int J Inf Commun Technol 13(1):34\u201354","journal-title":"Int J Inf Commun Technol"},{"key":"4181_CR4","volume-title":"The B-book: assigning programs to meanings","author":"JR Abrial","year":"2005","unstructured":"Abrial JR (2005) The B-book: assigning programs to meanings. Cambridge University Press, Cambridge"},{"issue":"1","key":"4181_CR5","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10270-008-0110-3","volume":"9","author":"K Anastasakis","year":"2010","unstructured":"Anastasakis K, Bordbar B, Georg G, Ray I (2010) On challenges of model transformation from UML to Alloy. Softw Syst Model 9(1):69\u201386","journal-title":"Softw Syst Model"},{"key":"4181_CR6","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/j.entcs.2009.07.003","volume":"243","author":"P Ayrault","year":"2009","unstructured":"Ayrault P, Hardin T, Pessaux F (2009) Development life-cycle of critical software under FoCaL. Electron Notes Theor Comput Sci 243:15\u201331","journal-title":"Electron Notes Theor Comput Sci"},{"key":"4181_CR7","series-title":"LNAI","first-page":"1","volume-title":"Verification of object-oriented software: the key approach","author":"B Beckert","year":"2007","unstructured":"Beckert B, H\u00e4hnle R, Schmitt P (2007) Verification of object-oriented software: the key approach, vol 4334. LNAI. Springer, Berlin, pp 1\u201318"},{"key":"4181_CR8","doi-asserted-by":"crossref","unstructured":"Bonichon R, Delahaye D, Doligez D (2007) Zenon: an extensible automated theorem prover producing checkable proofs. In: Logic for programming, artificial intelligence, and reasoning. Springer, pp 151\u2013165","DOI":"10.1007\/978-3-540-75560-9_13"},{"key":"4181_CR9","unstructured":"Brucker A, Wolff B (2007) The HOL-OCL book. Swiss Federal Institute of Technolgy (ETH). http:\/\/www.brucker.ch\/ . Accessed 3 Dec 2019"},{"key":"4181_CR10","doi-asserted-by":"crossref","unstructured":"Cabot J, Claris\u00f3 R, Riera D (2007) Umltocsp: a tool for the formal verification of UML\/OCL models using constraint programming. In: Proceedings of the twenty-second IEEE\/ACM international conference on automated software engineering. ACM, pp 547\u2013548","DOI":"10.1145\/1321631.1321737"},{"issue":"3","key":"4181_CR11","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/S0167-6423(02)00092-8","volume":"46","author":"PJ Carreira","year":"2003","unstructured":"Carreira PJ, Costa ME (2003) Automatically verifying an object-oriented specification of the steam-boiler system. Sci Comput Program 46(3):197\u2013217","journal-title":"Sci Comput Program"},{"issue":"2","key":"4181_CR12","doi-asserted-by":"publisher","first-page":"48","DOI":"10.4018\/IJERTCS.2015040103","volume":"6","author":"W Chama","year":"2015","unstructured":"Chama W, Chaoui A, Rehab S (2015) Formal modeling and analysis of object oriented systems using triple graph grammars. Int J Embed Real-Time Commun Syst (IJERTCS) 6(2):48\u201364","journal-title":"Int J Embed Real-Time Commun Syst (IJERTCS)"},{"key":"4181_CR13","doi-asserted-by":"crossref","unstructured":"Clavel M, Egea M (2006) ITP\/OCL: a rewriting-based validation tool for UML+ OCL static class diagrams. In: 11th international conference on algebraic methodology and software technology. LNCS, vol 4019. Springer, pp 368\u2013373","DOI":"10.1007\/11784180_28"},{"key":"4181_CR14","volume-title":"All about Maude a high performance logical framework: how to specify, program and verify systems in rewriting logic","author":"M Clavel","year":"2007","unstructured":"Clavel M, Dur\u00e1n F, Eker S, Lincoln P, Mart\u00ed-Oliet N, Meseguer J, Talcott C (2007) All about Maude a high performance logical framework: how to specify, program and verify systems in rewriting logic. Springer, Berlin"},{"key":"4181_CR15","unstructured":"Coq (2016) The Coq Proof Assistant, tutorial and reference manual, version 8.5. INRIA\u2013LIP\u2013LRI\u2013LIX\u2013PPS. http:\/\/coq.inria.fr\/ . Accessed 3 Dec 2019"},{"issue":"1","key":"4181_CR16","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10270-013-0353-5","volume":"14","author":"A Cunha","year":"2013","unstructured":"Cunha A, Garis A, Riesco D (2013) Translating between Alloy specifications and UML class diagrams annotated with OCL constraints. Softw Syst Model 14(1):5\u201325","journal-title":"Softw Syst Model"},{"issue":"1","key":"4181_CR17","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10270-013-0353-5","volume":"14","author":"A Cunha","year":"2015","unstructured":"Cunha A, Garis A, Riesco D (2015) Translating between Alloy specifications and UML class diagrams annotated with OCL. Softw Syst Model 14(1):5\u201325","journal-title":"Softw Syst Model"},{"key":"4181_CR18","doi-asserted-by":"crossref","unstructured":"Delahaye D, \u00c9tienne J, Donzeau-Gouge V (2008a) Producing UML models from Focal specifications: an application to Airport Security Regulations. In: 2nd IFIP\/IEEE international symposium on theoretical aspects of software engineering, pp 121\u2013124","DOI":"10.1109\/TASE.2008.35"},{"issue":"3","key":"4181_CR19","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s11334-008-0060-5","volume":"4","author":"D Delahaye","year":"2008","unstructured":"Delahaye D, \u00c9tienne JF, Donzeau-Gouge VV (2008b) A formal and sound transformation from Focal to UML: an application to airport security regulations. Innov Syst Softw Eng 4(3):267\u2013274","journal-title":"Innov Syst Softw Eng"},{"key":"4181_CR20","unstructured":"Doligez D (2016) The Zenon Tool. Software and Documentations freely available at http:\/\/zenon-prover.org\/ . Accessed 3 Dec 2019"},{"key":"4181_CR21","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n F, Gogolla M, Rold\u00e1n M (2011) Tracing properties of UML and OCL models with Maude. arXiv preprint arXiv:1107.0068 [csSE]","DOI":"10.4204\/EPTCS.56.6"},{"key":"4181_CR22","doi-asserted-by":"crossref","unstructured":"Favre LM (2010) Formalization of MOF-based metamodels. In: Model driven architecture for reverse engineering technologies: strategic directions and system evolution, IGI Global, pp 49 \u201379","DOI":"10.4018\/978-1-61520-649-0.ch004"},{"key":"4181_CR23","unstructured":"Fechter S (2005) S\u00e9mantique des traits orient\u00e9s objet de FoCaL. Ph.D. thesis, Universit\u00e9 PARIS 6"},{"key":"4181_CR24","unstructured":"Hardin T, Francois P, Pierre W, Damien D (2016) FoCaLiZe : tutorial and reference manual, version 0.9.1. CNAM-INRIA-LIP6. http:\/\/focalize.inria.fr . Accessed 3 Dec 2019"},{"key":"4181_CR25","volume-title":"Software Abstractions: logic, language, and analysis","author":"D Jackson","year":"2012","unstructured":"Jackson D (2012) Software Abstractions: logic, language, and analysis. MIT Press, Cambridge"},{"issue":"1","key":"4181_CR26","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/s11704-012-2901-5","volume":"6","author":"W Ke","year":"2012","unstructured":"Ke W, Li X, Liu Z, Stolz V (2012) rCOS: a formal model-driven engineering method for component-based software. Front Comput Sci 6(1):17\u201339","journal-title":"Front Comput Sci"},{"key":"4181_CR27","doi-asserted-by":"crossref","unstructured":"Kwon G (2000) Rewrite rules and operational semantics for model checking UML statecharts. In: UML2000\u2014the Unified Modeling Language. LNCS, vol 1939. Springer, pp 528\u2013540","DOI":"10.1007\/3-540-40011-7_39"},{"key":"4181_CR28","unstructured":"Ledang H, Souqui\u00e8res J, Charles S et al (2003) Argouml+ B: Un Outil de Transformation Syst\u00e9matique de Sp\u00e9cifications UML en B. In: AFADL\u20192003, pp 3\u201318"},{"key":"4181_CR29","doi-asserted-by":"crossref","unstructured":"Lilius J, Paltor IP (1999) vUML: a tool for verifying UML models. In: 14th IEEE international conference on automated software engineering, pp 255\u2013258","DOI":"10.1109\/ASE.1999.802301"},{"key":"4181_CR30","unstructured":"Miller J, Mukerji J et al (2003) MDA guide. Object Management Group, Inc, version 101"},{"key":"4181_CR31","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/b96103","volume-title":"CASL reference manual: the complete documentation of the common algebraic specification language","author":"P Mosses","year":"2004","unstructured":"Mosses P (2004) CASL reference manual: the complete documentation of the common algebraic specification language, vol 2960. LNCS. Springer, Berlin"},{"issue":"99","key":"4181_CR32","first-page":"547","volume":"71","author":"A Nimiya","year":"2010","unstructured":"Nimiya A, Yokigawa T, Miyazaki H, Amasaki S, Sato Y, Hayase M (2010) Model checking consistency of UML diagrams using Alloy. World Acad Sci Eng Technol 71(99):547\u2013550","journal-title":"World Acad Sci Eng Technol"},{"key":"4181_CR33","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: a proof assistant for higher-order logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow T, Paulson LC, Wenzel M (2002) Isabelle\/HOL: a proof assistant for higher-order logic, vol 2283. LNCS. Springer, Berlin"},{"key":"4181_CR34","unstructured":"OMG (2014) OCL: object constraint language 2.4. http:\/\/www.omg.org\/spec\/OCL\/2.4 . Accessed 3 Dec 2019"},{"key":"4181_CR35","unstructured":"OMG (2015) UML: Unified Modeling Language, version 2.5. http:\/\/www.omg.org\/spec\/UML\/2.5\/PDF . Accessed 3 Dec 2019"},{"key":"4181_CR36","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/3-540-45314-8_13","volume-title":"Fundamental Approaches to Software Engineering","author":"Gianna Reggio","year":"2001","unstructured":"Reggio G, Cerioli M, Astesiano E (2001) Towards a rigorous semantics of UML supporting its multiview approach. In: Fundamental approaches to software engineering. LNCS 2029. Springer, Berlin, pp 171\u2013186"},{"issue":"2","key":"4181_CR37","doi-asserted-by":"publisher","first-page":"953","DOI":"10.1007\/s10270-013-0350-8","volume":"14","author":"G Rull","year":"2015","unstructured":"Rull G, Farr\u00e9 C, Queralt A, Teniente E, Urp\u00ed T (2015) AuRUS: explaining the validation of UML\/OCL conceptual schemas. Softw Syst Model 14(2):953\u2013980","journal-title":"Softw Syst Model"},{"issue":"4","key":"4181_CR38","doi-asserted-by":"publisher","first-page":"1557","DOI":"10.1007\/s10270-013-0391-z","volume":"14","author":"MY Said","year":"2015","unstructured":"Said MY, Butler M, Snook C (2015) A method of refinement in UML-B. Softw Syst Model 14(4):1557\u20131580","journal-title":"Softw Syst Model"},{"issue":"1","key":"4181_CR39","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1125808.1125811","volume":"15","author":"Colin Snook","year":"2006","unstructured":"Snook C, Butler M (2006a) U2B - a tool for translating UML-B models into B. ACA Trans Softw Eng Methodol 15:92\u2013122. https:\/\/doi.org\/10.1145\/1125808.1125811","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"4181_CR40","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1125808.1125811","volume":"15","author":"C Snook","year":"2006","unstructured":"Snook C, Butler M (2006b) UML-B: formal modeling and design aided by UML. ACM Trans Softw Eng Methodol 15:92\u2013122","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"4181_CR41","doi-asserted-by":"publisher","unstructured":"Tao L, Fengsheng J (2015) B formal modeling based on UML class. In: IEEE international conference on signal processing, communications and computing (ICSPCC), 2015. IEEE Conference Publications, pp 1\u20136. https:\/\/doi.org\/10.1109\/ICSPCC.2015.7338854","DOI":"10.1109\/ICSPCC.2015.7338854"},{"key":"4181_CR42","unstructured":"Truong N, Souqui\u00e8res J (2006) Verification of UML model elements using B. J Inf Sci Eng 22:357\u2013373"},{"key":"4181_CR43","unstructured":"W3C (2014) XSL transformations (XSLT) version 3.0, W3C recommendation, Oct 2014. http:\/\/www.w3.org\/TR\/2014\/WD-xslt-30-20141002\/ . Accessed 3 Dec 2019"},{"key":"4181_CR44","doi-asserted-by":"crossref","unstructured":"Yang J (2009) A framework for formalizing UML models with formal language rCOS. In: Fourth international conference on frontier of computer science and technology, 2009 (FCST\u201909). IEEE, pp 408\u2013416","DOI":"10.1109\/FCST.2009.72"}],"container-title":["Soft Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00500-019-04181-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00500-019-04181-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00500-019-04181-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,18]],"date-time":"2023-09-18T07:09:12Z","timestamp":1695020952000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00500-019-04181-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,13]]},"references-count":44,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,3]]}},"alternative-id":["4181"],"URL":"https:\/\/doi.org\/10.1007\/s00500-019-04181-2","relation":{},"ISSN":["1432-7643","1433-7479"],"issn-type":[{"value":"1432-7643","type":"print"},{"value":"1433-7479","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,13]]},"assertion":[{"value":"13 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Compliance with ethical standards"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"This article does not contain any studies with human participants or animals performed by any of the authors.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical approval"}}]}}