{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:00:58Z","timestamp":1750309258653,"version":"3.41.0"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2024,8,14]],"date-time":"2024-08-14T00:00:00Z","timestamp":1723593600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100002347","name":"Bundesministeriums f\u00fcr Bildung und Forschung","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100002347","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Dependable Intelligent Systems Lab and BMBF"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2024,9,30]]},"abstract":"<jats:p>\n            In this article, a formal generic framework for defining and reasoning about deterministic concurrency in synchronous systems is implemented in the\n            <jats:sc>Spin<\/jats:sc>\n            model checker. Concretely, the work implements the\n            <jats:italic>clock-synchronised shared memory<\/jats:italic>\n            (\n            <jats:sc>csm<\/jats:sc>\n            ) theory, which extends synchronous programming with more and higher-level\n            <jats:sc>csm<\/jats:sc>\n            \u00a0data types. These\n            <jats:sc>csm<\/jats:sc>\n            \u00a0data types are equipped with a synchronisation\n            <jats:italic>policy<\/jats:italic>\n            prescribing how concurrent calls to objects methods must be organised. In a policy constructive system, all methods of every object can be scheduled in a policy-conformant manner without deadlocking. In our framework, synchronous policies get codified as\n            <jats:sc>Promela<\/jats:sc>\n            never-claims. In this form, the model checker can search for executions (interleavings) that satisfy the synchronous product of all the never-claims, namely policy-conformant schedules for all the\n            <jats:sc>csm<\/jats:sc>\n            \u00a0objects. The existence of such policy-conformant schedules verifies that the concurrent synchronous system is deterministic. The approach of this article extends beyond a single semantics since it can handle the synchronous programming model as well as the various forms of the sequentially constructive model found in the literature.\n          <\/jats:p>","DOI":"10.1145\/3626188","type":"journal-article","created":{"date-parts":[[2023,10,2]],"date-time":"2023-10-02T08:51:57Z","timestamp":1696236717000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Synchronised Shared Memory and Model Checking"],"prefix":"10.1145","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8305-4247","authenticated-orcid":false,"given":"Joaqu\u00edn","family":"Aguado","sequence":"first","affiliation":[{"name":"Otto-Friedrich-Universit\u00e4t Bamberg, Bamberg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3622-2505","authenticated-orcid":false,"given":"Alejandra","family":"Duenas","sequence":"additional","affiliation":[{"name":"ICN Business School, CEREFIGE, Nancy, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,8,14]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.007"},{"key":"e_1_3_3_3_2","doi-asserted-by":"crossref","unstructured":"J. Aguado M. Mendler M. Pouzet P. Roop and R. von Hanxleden. 2018. Deterministic concurrency: A clock-synchronised shared memory approach. In Programming Languages and Systems. Lecture Notes in Computer Science Vol. 10801. Springer 86\u2013113.","DOI":"10.1007\/978-3-319-89884-1_4"},{"key":"e_1_3_3_4_2","doi-asserted-by":"crossref","unstructured":"J. Aguado M. Mendler R. von Hanxleden and I. Fuhrmann. 2014. Grounding synchronous deterministic concurrency in sequential programming. In Programming Languages and Systems. Lecture Notes in Computer Science Vol. 8410. Springer 229\u2013248.","DOI":"10.1007\/978-3-642-54833-8_13"},{"issue":"4","key":"e_1_3_3_5_2","first-page":"393","article-title":"Denotational fixed-point semantics for constructive scheduling of synchronous concurrency","volume":"52","author":"Aguado J.","year":"2015","unstructured":"J. Aguado, M. Mendler, R. von Hanxleden, and I. Fuhrmann. 2015. Denotational fixed-point semantics for constructive scheduling of synchronous concurrency. Acta Informatica, Special Issue on Combining Compositionality and Concurrency 52, 4 (2015), 393\u2013442.","journal-title":"Acta Informatica, Special Issue on Combining Compositionality and Concurrency"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0161-5"},{"issue":"3","key":"e_1_3_3_7_2","first-page":"417","article-title":"Objects and synchronous programming","volume":"31","author":"Andr\u00e9 C.","year":"1997","unstructured":"C. Andr\u00e9, F. Boulanger, M.-A. P\u00e9raldi, J.-P. Rigault, and G. Vidal-Naquet. 1997. Objects and synchronous programming. RAIRO-APII-JESA: Journal Europeen des Systemes Automatises 31, 3 (1997), 417\u2013432.","journal-title":"RAIRO-APII-JESA: Journal Europeen des Systemes Automatises"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.5555\/647246.719617"},{"key":"e_1_3_3_9_2","volume-title":"Principles of Model Checking","author":"Baier C.","year":"2008","unstructured":"C. Baier and K. Joost-Pieter. 2008. Principles of Model Checking. MIT Press, Cambridge, MA."},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/5641.003.0021"},{"key":"e_1_3_3_11_2","volume-title":"The Constructive Semantics of Pure Esterel","author":"Berry G.","year":"2002","unstructured":"G. Berry. 2002. The Constructive Semantics of Pure Esterel. Draft Book Version 3, Sophia-Antipolis, France. https:\/\/www-sop.inria.fr\/members\/Gerard.Berry\/Papers\/EsterelConstructiveBook.pdf"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02997708"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"e_1_3_3_14_2","doi-asserted-by":"crossref","unstructured":"E. M. Clarke W. Klieber M. Nov\u00e1cek and P. Zuliani. 2011. Model checking and the state explosion problem. In Tools for Practical Software Verification. Lecture Notes in Computer Science Vol. 7682. Springer 1\u201330.","DOI":"10.1007\/978-3-642-35746-6_1"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/FDL50818.2020.9232942"},{"key":"e_1_3_3_16_2","doi-asserted-by":"crossref","unstructured":"N. Halbwachs. 1998. Synchronous programming of reactive systems a tutorial and commented bibliography. In Computer Aided Verification. Lecture Notes in Computer Science Vol. 1427. Springer 1\u201316.","DOI":"10.1007\/BFb0028726"},{"key":"e_1_3_3_17_2","doi-asserted-by":"crossref","unstructured":"N. Halbwachs F. Lagnier and P. Raymond. 1993. Synchronous observers and the verification of reactive systems. In Algebraic Methodology and Software Technology (AMAST\u201993). Workshops in Computing. Springer 83\u201396.","DOI":"10.1007\/978-1-4471-3227-1_8"},{"key":"e_1_3_3_18_2","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"Holzmann G.","year":"2004","unstructured":"G. Holzmann. 2004. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley."},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.5555\/1534411"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54624-2_6"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453482"},{"key":"e_1_3_3_22_2","volume-title":"Model Checking for SCCharts","author":"Stange A.-A.","year":"2019","unstructured":"A.-A. Stange. 2019. Model Checking for SCCharts. Master\u2019s Thesis. Department of Computer Science, Kiel University. Kiel, Germany. https:\/\/rtsys.informatik.uni-kiel.de\/biblio\/downloads\/theses\/aas-mt.pdf"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.1998.666789"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.04.009"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2627350"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3626188","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3626188","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:57:03Z","timestamp":1750291023000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3626188"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,14]]},"references-count":24,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2024,9,30]]}},"alternative-id":["10.1145\/3626188"],"URL":"https:\/\/doi.org\/10.1145\/3626188","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2024,8,14]]},"assertion":[{"value":"2022-01-31","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-07-14","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}