{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:42:37Z","timestamp":1740141757778,"version":"3.37.3"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2020,7,29]],"date-time":"2020-07-29T00:00:00Z","timestamp":1595980800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,7,29]],"date-time":"2020-07-29T00:00:00Z","timestamp":1595980800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100011914","name":"M\u00e4lardalen University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100011914","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2021,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Many database management systems (DBMS) need to ensure atomicity and isolation of transactions for logical data consistency, as well as to guarantee temporal correctness of the executed transactions. Since the mechanisms for atomicity and isolation may lead to breaching temporal correctness, trade-offs between these properties are often required during the DBMS design. To be able to address this concern, we have previously proposed the pattern-based UPPCART framework, which models the transactions and the DBMS mechanisms as timed automata, and verifies the trade-offs with provable guarantee. However, the manual construction of UPPCART models can require considerable effort and is prone to errors. In this paper, we advance the formal analysis of atomic concurrent real-time transactions with tool-automated construction of UPPCART models. The latter are generated automatically from our previously proposed UTRAN specifications, which are high-level UML-based specifications familiar to designers. To achieve this, we first propose formal definitions for the modeling patterns in UPPCART, as well as for the pattern-based construction of DBMS models, respectively. Based on this, we establish a translational semantics from UTRAN specifications to UPPCART models, to provide the former with a formal semantics relying on timed automata, and develop a tool that implements the automated transformation. We also extend the expressiveness of UTRAN and UPPCART, to incorporate transaction sequences and their timing properties. We demonstrate the specification in UTRAN, automated transformation to UPPCART, and verification of the traded-off properties, via an industrial use case.<\/jats:p>","DOI":"10.1007\/s10270-020-00819-0","type":"journal-article","created":{"date-parts":[[2020,7,29]],"date-time":"2020-07-29T06:03:44Z","timestamp":1596002624000},"page":"557-589","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Specification and automated verification of atomic concurrent real-time transactions"],"prefix":"10.1007","volume":"20","author":[{"given":"Simin","family":"Cai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Barbara","family":"Gallina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dag","family":"Nystr\u00f6m","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cristina","family":"Seceleanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,7,29]]},"reference":[{"key":"819_CR1","volume-title":"Transaction Processing: Concepts and Techniques","author":"J Gray","year":"1992","unstructured":"Gray, J., Reuter, A.: Transaction Processing: Concepts and Techniques. Morgan Kaufmann Publishers Inc., Burlington (1992)"},{"key":"819_CR2","volume-title":"Fundamentals of Database Systems","author":"RA Elmasri","year":"2004","unstructured":"Elmasri, R.A., Navathe, S.B.: Fundamentals of Database Systems. Addison-Wesley Longman Publishing Co. Inc, Boston (2004)"},{"key":"819_CR3","doi-asserted-by":"publisher","first-page":"2325","DOI":"10.1109\/TKDE.2012.173","volume":"25","author":"S Han","year":"2013","unstructured":"Han, S., et al.: On co-scheduling of update and control transactions in real-time sensing and control systems: algorithms, analysis, and performance. IEEE Trans. Knowl. Data Eng. 25, 2325\u20132342 (2013)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"819_CR4","doi-asserted-by":"crossref","unstructured":"Cai S., Gallina, B., Nystr\u00f6m, D., Seceleanu, C.: Customized real-time data management for automotive systems: a case study. In: The 43rd Annual Conference of the IEEE Industrial Electronics Society, pp. 8397\u20138404 (2017)","DOI":"10.1109\/IECON.2017.8217475"},{"issue":"2","key":"819_CR5","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/BF01264051","volume":"1","author":"K Ramamritham","year":"1993","unstructured":"Ramamritham, K.: Real-time databases. Distrib Parallel Databases 1(2), 199\u2013226 (1993)","journal-title":"Distrib Parallel Databases"},{"issue":"6","key":"819_CR6","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1109\/2.769440","volume":"32","author":"JA Stankovic","year":"1999","unstructured":"Stankovic, J.A., et al.: Misconceptions about real-time databases. Computer 32(6), 29\u201336 (1999)","journal-title":"Computer"},{"key":"819_CR7","unstructured":"Gallina, B.: PRISMA: a software product line-oriented process for the requirements engineering of flexible transaction models, Ph.D. thesis, University of Luxembourg (2010)"},{"key":"819_CR8","doi-asserted-by":"crossref","unstructured":"Cai, S., Gallina, B., Nystr\u00f6m, D., Seceleanu, C.: Specification and formal verification of atomic concurrent real-time transactions. In: The 23rd IEEE Pacific Rim International Symposium on Dependable Computing (2018)","DOI":"10.1109\/PRDC.2018.00021"},{"key":"819_CR9","unstructured":"The unified modeling language specification version 2.5.1, Standard, OMG. https:\/\/www.omg.org\/spec\/UML\/2.5.1\/. Accessed on 09 Jan 2019"},{"key":"819_CR10","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K Larsen","year":"1997","unstructured":"Larsen, K., et al.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer 1, 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"819_CR11","unstructured":"Object Constraint Language version 2.4, Standard, OMG. https:\/\/www.omg.org\/spec\/OCL\/2.4. Accessed on 09 Jan 2019"},{"key":"819_CR12","unstructured":"Cai, S.: The code repository. Password: SOSYM2019. https:\/\/www.idt.mdh.se\/personal\/sica\/sosym\/. Accessed on 30 Aug 2019"},{"key":"819_CR13","unstructured":"Derks, W., Dehnert, J., Grefen, P., Jonker, W.: Customized atomicity specification for transactional workflows. In: The Proceedings of the 3rd International Symposium on Cooperative Database Systems for Advanced Applications, pp. 140\u2013147 (2001)"},{"key":"819_CR14","unstructured":"Adya, A., et\u00a0al.: Generalized isolation level definitions. In: Proceedings of the 16th International Conference on Data Engineering, pp. 67\u201378 (2000)"},{"key":"819_CR15","unstructured":"ISO\/IEC 9075:1992 Database Language SQL, Standard, International Organization for Standardization"},{"key":"819_CR16","doi-asserted-by":"crossref","unstructured":"Soparkar, N., et\u00a0al.: Adaptive commitment for distributed real-time transactions. In: Proceedings of the third Conference on Information and Knowledge Management, pp. 187\u2013194 (1994)","DOI":"10.1145\/191246.191276"},{"key":"819_CR17","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1145\/132271.132276","volume":"17","author":"RK Abbott","year":"1992","unstructured":"Abbott, R.K., Garcia-Molina, H.: Scheduling real-time transactions: a performance evaluation. ACM Trans. Database Syst. 17, 513\u2013560 (1992)","journal-title":"ACM Trans. Database Syst."},{"key":"819_CR18","unstructured":"UML profile for marte specification version 1.1, Standard, OMG. https:\/\/www.omg.org\/spec\/MARTE\/1.1\/"},{"key":"819_CR19","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency, vol. 84. Prentice Hall, Upper Saddle River (1989)"},{"issue":"2","key":"819_CR20","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., et al.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"819_CR21","doi-asserted-by":"crossref","unstructured":"Cai, S., Gallina, B., Nystr\u00f6m, D., Seceleanu, C.: A formal approach for flexible modeling and analysis of transaction timeliness and isolation. In: Proceedings of the 24th International Conference on Real-Time Networks and Systems, pp. 3\u201312 (2016)","DOI":"10.1145\/2997465.2997495"},{"key":"819_CR22","unstructured":"Cai, S., Gallina, B., Nystr\u00f6m, D., Seceleanu, C.: Specification and automated verification of atomic concurrent real-time transactions: extended report. Tech. rep. http:\/\/www.es.mdh.se\/publications\/5792-"},{"key":"819_CR23","doi-asserted-by":"crossref","unstructured":"Mottu, J.-M., Baudry, B., Le\u00a0Traon, Y.: Model transformation testing: oracle issue. In: 2008 IEEE International Conference on Software Testing Verification and Validation Workshop, IEEE, pp. 105\u2013112 (2008)","DOI":"10.1109\/ICSTW.2008.27"},{"key":"819_CR24","doi-asserted-by":"crossref","unstructured":"Biliris, A., Dar, S., Gehani, N., Jagadish, H., Ramamritham, K.: ASSET: A system for supporting extended transactions. In: ACM SIGMOD Record, vol. 23, pp. 44\u201354 (1994)","DOI":"10.1145\/191843.191848"},{"key":"819_CR25","doi-asserted-by":"crossref","unstructured":"Fabry, J., D\u2019Hondt, T.: KALA: Kernel aspect language for advanced transactions. In: Proceedings of the 2006 ACM Symposium on Applied Computing, pp. 1615\u20131620 (2006)","DOI":"10.1145\/1141277.1141655"},{"key":"819_CR26","doi-asserted-by":"crossref","unstructured":"Arntsen, A.-B., Karlsen, R.: Reflects: a flexible transaction service framework. In: Proceedings of the 4th Workshop on Reflective and Adaptive Middleware Systems, ACM, p.\u00a04 (2005)","DOI":"10.1145\/1101516.1101520"},{"key":"819_CR27","unstructured":"Marouane, H., Duvallet, C., Makni, A., Bouaziz, R., Sadeg, B.: An UML profile for representing real-time design patterns. J King Saud Univ. Comput. Inf. Sci"},{"key":"819_CR28","unstructured":"Nektarios, G., Christodoulakis, S.: UTML: Unified transaction modeling language. In: Proceedings of the 3rd International Conference on Web Information Systems Engineering, pp. 115\u2013126 (2002)"},{"issue":"1","key":"819_CR29","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1504\/IJWET.2007.011527","volume":"3","author":"D Distante","year":"2006","unstructured":"Distante, D., Rossi, G., Canfora, G., Tilley, S.: A comprehensive design model for integrating business processes in web applications. Int. J. Web Eng. Technol. 3(1), 43\u201372 (2006)","journal-title":"Int. J. Web Eng. Technol."},{"key":"819_CR30","unstructured":"Web services business process execution language version 2.0, Standard, OASIS. http:\/\/docs.oasis-open.org\/wsbpel\/2.0\/OS\/wsbpel-v2.0-OS.html"},{"key":"819_CR31","unstructured":"Business process model and notation specification version 2.0, Standard, OMG. https:\/\/www.omg.org\/spec\/BPMN\/2.0\/"},{"key":"819_CR32","doi-asserted-by":"crossref","unstructured":"Charfi, A., Schmeling, B., Mezini, M.: Transactional BPEL processes with AO4BPEL aspects. In: Fifth European Conference on Web Services, pp. 149\u2013158 (2007)","DOI":"10.1109\/ECOWS.2007.17"},{"issue":"2","key":"819_CR33","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1109\/TSC.2010.50","volume":"4","author":"C-A Sun","year":"2011","unstructured":"Sun, C.-A., el Khoury, E., Aiello, M.: Transaction management in service-oriented systems: requirements and a proposal. IEEE Trans. Serv. Comput. 4(2), 167\u2013180 (2011)","journal-title":"IEEE Trans. Serv. Comput."},{"key":"819_CR34","doi-asserted-by":"crossref","unstructured":"Watahiki, K., Ishikawa, F., Hiraishi, K.: Formal verification of business processes with temporal and resource constraints. In: IEEE International Conference on Systems, Man, and Cybernetics, pp. 1173\u20131180 (2011)","DOI":"10.1109\/ICSMC.2011.6083857"},{"key":"819_CR35","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1145\/185827.185843","volume":"19","author":"PK Chrysanthis","year":"1994","unstructured":"Chrysanthis, P.K., Ramamritham, K.: Synthesis of extended transaction models using ACTA. ACM Trans. Database Syst. 19, 450\u2013491 (1994)","journal-title":"ACM Trans. Database Syst."},{"key":"819_CR36","doi-asserted-by":"crossref","unstructured":"Liu, S., \u00d6lveczky, P.\u00a0C., Rahman, M.R., Ganhotra, J., Gupta, I., Meseguer, J.: Formal modeling and analysis of RAMP transaction systems. In: Proceedings of the 31st Annual ACM Symposium on Applied Computing, pp. 1700\u20131707 (2016)","DOI":"10.1145\/2851613.2851838"},{"key":"819_CR37","doi-asserted-by":"crossref","unstructured":"Lanotte, R., Maggiolo-Schettini, A., Milazzo, P., Troina, A.: Modeling long-running transactions with communicating hierarchical timed automata. In: Formal Methods for Open Object-Based Distributed Systems, Springer, pp. 108\u2013122 (2006)","DOI":"10.1007\/11768869_10"},{"key":"819_CR38","doi-asserted-by":"crossref","unstructured":"Cai, S., Gallina, B., Nystr\u00f6m, D., Seceleanu, C.: Statistical model checking for real-time database management systems: a case study. In: Proceedings of the 24th IEEE Conference on Emerging Technologies and Factory Automation (ETFA), IEEE (2019)","DOI":"10.1109\/ETFA.2019.8869326"},{"key":"819_CR39","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B., Van\u00a0Vliet, J., Wang, Z.: Statistical model checking for networks of priced timed automata. In: International Conference on Formal Modeling and Analysis of Timed Systems, Springer, pp. 80\u201396 (2011)","DOI":"10.1007\/978-3-642-24310-3_7"},{"issue":"6","key":"819_CR40","doi-asserted-by":"publisher","first-page":"844","DOI":"10.1109\/TSE.2008.52","volume":"34","author":"JS Dong","year":"2008","unstructured":"Dong, J.S., Hao, P., Qin, S., Sun, J., Yi, W.: Timed automata patterns. IEEE Trans. Software Eng. 34(6), 844\u2013859 (2008)","journal-title":"IEEE Trans. Software Eng."},{"key":"819_CR41","doi-asserted-by":"crossref","unstructured":"Mekki, A., Ghazel, M., Toguyeni, A.: Validating time-constrained systems using UML statecharts patterns and timed automata observers. In: 3rd International Workshop on Verification and Evaluation of Computer and Communication Systems (2009)","DOI":"10.14236\/ewic\/VECOS2009.11"},{"key":"819_CR42","doi-asserted-by":"crossref","unstructured":"Andr\u00e9, \u00c9.: Observer patterns for real-time systems. In: 2013 18th International Conference on Engineering of Complex Computer Systems, IEEE, pp. 125\u2013134 (2013)","DOI":"10.1109\/ICECCS.2013.26"},{"issue":"4","key":"819_CR43","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1145\/1755951.1755907","volume":"45","author":"M Biehl","year":"2010","unstructured":"Biehl, M., DeJiu, C., T\u00f6rngren, M.: Integrating safety analysis into the model-based development toolchain of automotive embedded systems. ACM SIGPLAN Not. 45(4), 125\u2013132 (2010)","journal-title":"ACM SIGPLAN Not."},{"key":"819_CR44","doi-asserted-by":"crossref","unstructured":"Enoiu, E.P., Marinescu, R., Seceleanu, C., Pettersson, P.: ViTAL: A verification tool for east-adl models using uppaal por. In: Proceedings of the 17th International Conference on Engineering of Complex Computer Systems, IEEE, pp. 328\u2013337 (2012)","DOI":"10.1109\/ICECCS20050.2012.6299228"},{"key":"819_CR45","unstructured":"Mazzini, S., Favaro, J.M., Puri, S., Baracchi, L.: CHESS: an open source methodology and toolset for the development of critical systems. In: EduSymp\/OSS4MDE@ MoDELS, pp. 59\u201366 (2016)"},{"key":"819_CR46","unstructured":"Moss, E.B.: Nested transactions: an approach to reliable distributed computing. Massachusetts Institute of Technology, USA. Ph.D. thesis (1981)"},{"issue":"3","key":"819_CR47","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1145\/38714.38742","volume":"16","author":"H Garcia-Molina","year":"1987","unstructured":"Garcia-Molina, H., Salem, K.: SAGAS. ACM Sigmod Record 16(3), 249\u2013259 (1987)","journal-title":"ACM Sigmod Record"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00819-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-020-00819-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00819-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,28]],"date-time":"2021-07-28T23:04:33Z","timestamp":1627513473000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-020-00819-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,29]]},"references-count":47,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,4]]}},"alternative-id":["819"],"URL":"https:\/\/doi.org\/10.1007\/s10270-020-00819-0","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2020,7,29]]},"assertion":[{"value":"5 September 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 April 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 July 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 July 2020","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}