{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,11,30]],"date-time":"2023-11-30T23:54:07Z","timestamp":1701388447935},"reference-count":23,"publisher":"Wiley","issue":"7","license":[{"start":{"date-parts":[[2012,2,14]],"date-time":"2012-02-14T00:00:00Z","timestamp":1329177600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Concurrency and Computation"],"published-print":{"date-parts":[[2012,5]]},"abstract":"SUMMARY<\/jats:title>In modern transaction processing software, the ACID properties (atomicity, consistency, isolation, durability) are often relaxed, in order to address requirements that arise in computing environments of today. Typical examples are the long\u2010running transactions in mobile computing, in service\u2010oriented architectures and B2B collaborative applications. These new transaction models are collectively known as advanced or extended transactions. Formal specification and reasoning for transaction properties have been limited to proof\u2010theoretic approaches, despite the recent progress in model checking. In this work, we present a model\u2010driven approach for generating a provably correct implementation of the transaction model of interest. The model is specified by state machines for the transaction participants, which are synchronized on a set of events. All possible execution paths of the synchronized state machines are checked for property violations. An implementation for the verified transaction model is then automatically generated. To demonstrate the approach, the specification of nested transactions is verified, because it is the basis for many advanced transaction models. Concurrency and Computation: Practice and Experience<\/jats:italic>. Copyright \u00a9 2012 John Wiley & Sons, Ltd.<\/jats:p>","DOI":"10.1002\/cpe.1876","type":"journal-article","created":{"date-parts":[[2012,2,15]],"date-time":"2012-02-15T03:38:20Z","timestamp":1329277100000},"page":"711-722","source":"Crossref","is-referenced-by-count":6,"title":["Model checking and code generation for transaction processing software"],"prefix":"10.1002","volume":"24","author":[{"given":"Anakreon","family":"Mentis","sequence":"first","affiliation":[{"name":"Department of Informatics Aristotle University of Thessaloniki Thessaloniki 54124 Greece"}]},{"given":"Panagiotis","family":"Katsaros","sequence":"additional","affiliation":[{"name":"Department of Informatics Aristotle University of Thessaloniki Thessaloniki 54124 Greece"}]}],"member":"311","published-online":{"date-parts":[[2012,2,14]]},"reference":[{"key":"e_1_2_11_2_1","volume-title":"Transactional Information Systems","author":"Weikum G","year":"2002"},{"key":"e_1_2_11_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10619-008-7028-1"},{"key":"e_1_2_11_4_1","doi-asserted-by":"crossref","first-page":"557","DOI":"10.1007\/978-0-387-39940-9_95","article-title":"Data broadcasting, caching and replication in mobile computing","author":"Chrysanthis PK","year":"2009","journal-title":"Encyclopedia of Database Systems"},{"key":"e_1_2_11_5_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:DAPD.0000028552.69032.f9"},{"key":"e_1_2_11_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.elerap.2005.10.010"},{"key":"e_1_2_11_7_1","volume-title":"Model\u2010Driven Software Development: Technology, Engineering, Management","author":"Stahl T","year":"2005"},{"key":"e_1_2_11_8_1","volume-title":"Model Checking","author":"Clarke EM","year":"2000"},{"key":"e_1_2_11_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17187-8_42"},{"key":"e_1_2_11_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/185827.185843"},{"key":"e_1_2_11_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.02.022"},{"key":"e_1_2_11_12_1","volume-title":"The SPIN Model Checker \u2013 Primer and Reference Manual","author":"Holzmann GJ","year":"2003"},{"key":"e_1_2_11_13_1","unstructured":"ACID Model Checker & Code Generator.http:\/\/mathind.csd.auth.gr\/acid\/html\/[27 September2010]."},{"key":"e_1_2_11_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCSIM.2009.5191824"},{"key":"e_1_2_11_15_1","doi-asserted-by":"publisher","DOI":"10.4108\/ICST.SIMUTOOLS2008.3113"},{"key":"e_1_2_11_16_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.1059"},{"key":"e_1_2_11_17_1","unstructured":"EliotJ MossB.Nested transactions: an approach to reliable distributed computing.Tech. Report MIT\/LCS\/TR\u2010260 Massachusetts Institute of Technology 1981."},{"key":"e_1_2_11_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04558-9"},{"issue":"1","key":"e_1_2_11_19_1","first-page":"0","article-title":"The Haskell 98 language and libraries: the revised report","volume":"13","author":"Jones P","year":"2003","journal-title":"Journal of Functional Programming"},{"key":"e_1_2_11_20_1","volume-title":"Principles of Model Checking","author":"Baier C","year":"2008"},{"key":"e_1_2_11_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/93597.98729"},{"key":"e_1_2_11_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_11_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEAA.2009.84"},{"key":"e_1_2_11_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2010.07.006"}],"container-title":["Concurrency and Computation: Practice and Experience"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fcpe.1876","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/cpe.1876","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,12]],"date-time":"2023-09-12T14:53:44Z","timestamp":1694530424000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/cpe.1876"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,2,14]]},"references-count":23,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2012,5]]}},"alternative-id":["10.1002\/cpe.1876"],"URL":"https:\/\/doi.org\/10.1002\/cpe.1876","archive":["Portico"],"relation":{},"ISSN":["1532-0626","1532-0634"],"issn-type":[{"value":"1532-0626","type":"print"},{"value":"1532-0634","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,2,14]]}}}