{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T04:53:44Z","timestamp":1755838424344,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466742"},{"type":"electronic","value":"9783662466759"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46675-9_15","type":"book-chapter","created":{"date-parts":[[2015,3,31]],"date-time":"2015-03-31T16:24:38Z","timestamp":1427819078000},"page":"218-232","source":"Crossref","is-referenced-by-count":1,"title":["Model-Based Formal Reasoning about Data-Management Applications"],"prefix":"10.1007","author":[{"given":"Carolina","family":"Dania","sequence":"first","affiliation":[]},{"given":"Manuel","family":"Clavel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"15_CR1","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1145\/1125808.1125810","volume":"15","author":"David Basin","year":"2006","unstructured":"Basin, D., Doser, J., Lodderstedt, T.: Model driven security: From UML models to access control infrastructures. ACM Transactions on Software Engineering and Methodology\u00a015(1), 39\u201391 (2006)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"issue":"4","key":"15_CR2","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1109\/TSE.2013.2297116","volume":"40","author":"D.A. Basin","year":"2014","unstructured":"Basin, D.A., Clavel, M., Egea, M., Garc\u00eda de Dios, M.A., Dania, C.: A model-driven methodology for developing secure data-management applications. IEEE Trans. Software Eng.\u00a040(4), 324\u2013337 (2014)","journal-title":"IEEE Trans. Software Eng."},{"issue":"2","key":"15_CR3","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1016\/j.jss.2009.08.012","volume":"83","author":"J. Cabot","year":"2010","unstructured":"Cabot, J., Claris\u00f3, R., Guerra, E., de Lara, J.: Verification and validation of declarative model-to-model transformations through invariants. Journal of Systems and Software\u00a083(2), 283\u2013302 (2010)","journal-title":"Journal of Systems and Software"},{"key":"15_CR4","first-page":"1","volume":"24","author":"M. Clavel","year":"2009","unstructured":"Clavel, M., Egea, M., Garc\u00eda de Dios, M.A.: Checking unsatisfiability for OCL constraints. Electronic Communications of the EASST\u00a024, 1\u201313 (2009)","journal-title":"Electronic Communications of the EASST"},{"key":"15_CR5","unstructured":"Dania, C., Clavel, M.: OCL2FOL+: Coping with Undefinedness. In: Cabot, J., Gogolla, M., R\u00e1th, I., Willink, E. (eds.) CEUR Workshop Proceedings OCL@MoDELS, vol.\u00a01092, pp. 53\u201362. CEUR-WS.org (2013)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-07452-8_4","volume-title":"Engineering Secure Future Internet Services and Systems","author":"M.A. Dios Garc\u00eda de","year":"2014","unstructured":"Garc\u00eda de Dios, M.A., Dania, C., Basin, D., Clavel, M.: Model-driven development of a secure eHealth application. In: Heisel, M., Joosen, W., Lopez, J., Martinelli, F. (eds.) Engineering Secure Future Internet Services and Systems. LNCS, vol.\u00a08431, pp. 97\u2013118. Springer, Heidelberg (2014)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"15_CR8","unstructured":"D\u2019Souza, D., Wills, A.: Catalysis. Practical Rigor and Refinement: Extending OMT, Fusion, and Objectory. Technical report (1995), \n                      \n                        http:\/\/catalysis.org"},{"key":"15_CR9","unstructured":"Gogolla, M., Hamann, L., Hilken, F., Kuhlmann, M., France, R.B.: From application models to filmstrip models: An approach to automatic validation of model dynamics. In: Fill, H., Karagiannis, D., Reimer, U. (eds.) Modellierung. LNI, vol.\u00a0225, pp. 273\u2013288. GI (2014)"},{"issue":"8","key":"15_CR10","doi-asserted-by":"publisher","first-page":"821","DOI":"10.1016\/j.infsof.2014.03.003","volume":"56","author":"C.A. Gonz\u00e1lez","year":"2014","unstructured":"Gonz\u00e1lez, C.A., Cabot, J.: Formal verification of static software models in MDE: A systematic review. Information & Software Technology\u00a056(8), 821\u2013838 (2014)","journal-title":"Information & Software Technology"},{"key":"15_CR11","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press (2006)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-36089-3_6","volume-title":"Software Language Engineering","author":"B. Kanso","year":"2013","unstructured":"Kanso, B., Taha, S.: Temporal constraint support for OCL. In: Czarnecki, K., Hedin, G. (eds.) SLE 2012. LNCS, vol.\u00a07745, pp. 83\u2013103. Springer, Heidelberg (2013)"},{"key":"15_CR13","volume-title":"MDA Explained: The Model Driven Architecture: Practice and Promise","author":"A.G. Kleppe","year":"2003","unstructured":"Kleppe, A.G., Warmer, J., Bast, W.: MDA Explained: The Model Driven Architecture: Practice and Promise. Addison-Wesley Longman Publishing Co., Inc., Boston (2003)"},{"key":"15_CR14","unstructured":"NESSoS. The European Network of Excellence on Engineering Secure Future internet Software Services and Systems (2010), \n                      \n                        http:\/\/www.nessos-project.eu"},{"key":"15_CR15","unstructured":"Object Management Group. Object constraint language specification version 2.4. Technical report, OMG (2014), \n                      \n                        http:\/\/www.omg.org\/spec\/OCL\/2.4"},{"key":"15_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.datak.2011.09.004","volume":"73","author":"A. Queralt","year":"2012","unstructured":"Queralt, A., Artale, A., Calvanese, D., Teniente, E.: OCL-Lite: Finite reasoning on UML\/OCL conceptual schemas. Data & Knowledge Engineering\u00a073, 1\u201322 (2012)","journal-title":"Data & Knowledge Engineering"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML\/OCL models using Boolean satisfiability. In: DATE, pp. 1341\u20131344. IEEE (2010)","DOI":"10.1109\/DATE.2010.5457017"},{"issue":"4","key":"15_CR18","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1145\/299917.299919","volume":"30","author":"R. WieringaA","year":"1998","unstructured":"WieringaA, R.: survey of structured and object-oriented software specification methods and techniques. ACM Comput. Surv.\u00a030(4), 459\u2013527 (1998)","journal-title":"ACM Comput. Surv."}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46675-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T23:27:45Z","timestamp":1558308465000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46675-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466742","9783662466759"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46675-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}