{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,8]],"date-time":"2025-12-08T22:02:44Z","timestamp":1765231364698,"version":"3.41.2"},"reference-count":53,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2024,7,3]],"date-time":"2024-07-03T00:00:00Z","timestamp":1719964800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,7,3]],"date-time":"2024-07-03T00:00:00Z","timestamp":1719964800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100004054","name":"King Abdulaziz University","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004054","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100012171","name":"Ontario Research Foundation","doi-asserted-by":"publisher","award":["CyPreSS: Software Techniques for the Engineering o"],"award-info":[{"award-number":["CyPreSS: Software Techniques for the Engineering o"]}],"id":[{"id":"10.13039\/100012171","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100018693","name":"HORIZON EUROPE Framework Programme","doi-asserted-by":"publisher","award":["Grant Agreement 101070537 - CrossCon"],"award-info":[{"award-number":["Grant Agreement 101070537 - CrossCon"]}],"id":[{"id":"10.13039\/100018693","id-type":"DOI","asserted-by":"publisher"}]},{"name":"PNRR","award":["FAIR - Future AI Research"],"award-info":[{"award-number":["FAIR - Future AI Research"]}]},{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["Middleware Framework and Programming Infrastructur"],"award-info":[{"award-number":["Middleware Framework and Programming Infrastructur"]}],"id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000155","name":"Social Sciences and Humanities Research Council of Canada","doi-asserted-by":"publisher","award":["Autonomy Through Cyberjustice Technologies"],"award-info":[{"award-number":["Autonomy Through Cyberjustice Technologies"]}],"id":[{"id":"10.13039\/501100000155","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2025,8]]},"DOI":"10.1007\/s10270-024-01180-2","type":"journal-article","created":{"date-parts":[[2024,7,3]],"date-time":"2024-07-03T13:02:00Z","timestamp":1720011720000},"page":"1093-1126","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["SymboleoPC: checking properties of legal contracts"],"prefix":"10.1007","volume":"24","author":[{"given":"Alireza","family":"Parvizimosaed","sequence":"first","affiliation":[]},{"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[]},{"given":"Aidin","family":"Rasti","sequence":"additional","affiliation":[]},{"given":"Amal Ahmed","family":"Anda","sequence":"additional","affiliation":[]},{"given":"Sofana","family":"Alfuhaid","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2414-1791","authenticated-orcid":false,"given":"Daniel","family":"Amyot","sequence":"additional","affiliation":[]},{"given":"Luigi","family":"Logrippo","sequence":"additional","affiliation":[]},{"given":"John","family":"Mylopoulos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,3]]},"reference":[{"key":"1180_CR1","unstructured":"Aberer, K., Hauswirth, M., Salehi, A.: Middleware support for the \u201cInternet of Things\u201d. In: 5th GI\/ITG KuVS Fachgespr\u00e4ch \u201cDrahtlose Sensornetze\u201d, pp. 15\u201320. Universit\u00e4t Stuttgart, Germany, (2006). https:\/\/elib.uni-stuttgart.de\/bitstream\/11682\/2604\/1\/TR_2006_07.pdf"},{"issue":"4","key":"1180_CR2","doi-asserted-by":"publisher","first-page":"9","DOI":"10.2753\/JEC1086-4415120401","volume":"12","author":"M Alberti","year":"2008","unstructured":"Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Montali, M., Torroni, P.: Expressing and verifying business contracts with abductive logic programming. Int. J. Electron. Commer. 12(4), 9\u201338 (2008). https:\/\/doi.org\/10.2753\/JEC1086-4415120401","journal-title":"Int. J. Electron. Commer."},{"key":"1180_CR3","doi-asserted-by":"publisher","unstructured":"Alqahtani, S.M., He, X., Gamble, R.\u00a0F., Papa, M.: Formal verification of functional requirements for smart contract compositions in supply chain management systems. In: 53rd Hawaii International Conference on System Sciences, HICSS 2020, pp. 1\u201310, (2020). https:\/\/doi.org\/10.24251\/HICSS.2020.650","DOI":"10.24251\/HICSS.2020.650"},{"key":"1180_CR4","unstructured":"Antonino, P., Roscoe, A.\u00a0W.: Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity. CoRR, (2020). arxiv: 2002.02710"},{"key":"1180_CR5","doi-asserted-by":"publisher","unstructured":"Barrett, C.\u00a0W., Sebastiani, R., Seshia, S.\u00a0A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pp. 825\u2013885. IOS Press, (2009). https:\/\/doi.org\/10.3233\/978-1-58603-929-5-825","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"1180_CR6","volume-title":"Implementing domain specific languages with Xtext and Xtend","author":"L Bettini","year":"2016","unstructured":"Bettini, L.: Implementing domain specific languages with Xtext and Xtend, 2nd edn. Packt Publishing (2016)","edition":"2"},{"key":"1180_CR7","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: Sat-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 70\u201387. Springer, Berlin Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"1180_CR8","doi-asserted-by":"publisher","unstructured":"Cavada, R., Cimatti, A., Micheli, A., Roveri, M., Susi, A., Tonetta, S.: Othelloplay: a plug-in based tool for requirement formalization and validation. In: TOPI@ICSE, p. 59. ACM, (2011). https:\/\/doi.org\/10.1145\/1984708.1984728","DOI":"10.1145\/1984708.1984728"},{"key":"1180_CR9","doi-asserted-by":"publisher","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Computer Aided Verification, pp. 334\u2013342, Springer, Cham, (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"issue":"1","key":"1180_CR10","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s10458-012-9202-0","volume":"27","author":"F Chesani","year":"2013","unstructured":"Chesani, F., Mello, P., Montali, M., Torroni, P.: Representing and monitoring social commitments using the event calculus. Auton. Agent. Multi-Agent Syst. 27(1), 85\u2013130 (2013). https:\/\/doi.org\/10.1007\/s10458-012-9202-0","journal-title":"Auton. Agent. Multi-Agent Syst."},{"key":"1180_CR11","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: Computer Aided Verification, pp. 359\u2013364. Springer Berlin Heidelberg, (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29","DOI":"10.1007\/3-540-45657-0_29"},{"issue":"4","key":"1180_CR12","doi-asserted-by":"publisher","first-page":"22:1","DOI":"10.1145\/2377656.2377659","volume":"21","author":"A Cimatti","year":"2012","unstructured":"Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: Validation of requirements for hybrid systems: a formal approach. ACM Trans. Softw. Eng. Methodol. 21(4), 22:1-22:34 (2012). https:\/\/doi.org\/10.1145\/2377656.2377659","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"1","key":"1180_CR13","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1008615614281","volume":"10","author":"EM Clarke","year":"1997","unstructured":"Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. Formal Methods Syst. Des. 10(1), 47\u201371 (1997). https:\/\/doi.org\/10.1023\/A:1008615614281","journal-title":"Formal Methods Syst. Des."},{"key":"1180_CR14","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press (2001). ISBN 978-0-262-03270-4. https:\/\/mitpress.mit.edu\/9780262038836\/model-checking\/"},{"key":"1180_CR15","unstructured":"CSM Lab. Symboleo IDE Tool, (2020). https:\/\/github.com\/Smart-Contract-Modelling-uOttawa\/Symboleo-IDE. Accessed 10-February-2022"},{"key":"1180_CR16","unstructured":"Daskalopulu, A.-K.: Logic-based tools for the analysis and representation of legal contracts. PhD thesis, Imperial College London, UK"},{"key":"1180_CR17","doi-asserted-by":"publisher","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: 1999 International Conference on Software Engineering, ICSE\u201999, pp. 411\u2013420. ACM, (1999). https:\/\/doi.org\/10.1145\/302405.302672","DOI":"10.1145\/302405.302672"},{"issue":"3","key":"1180_CR18","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"EA Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241\u2013266 (1982). https:\/\/doi.org\/10.1016\/0167-6423(83)90017-5","journal-title":"Sci. Comput. Program."},{"key":"1180_CR19","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1613\/jair.1129","volume":"20","author":"M Fox","year":"2003","unstructured":"Fox, M., Long, D.: PDDL2.1: an extension to PDDL for expressing temporal planning domains. J. Artif. Intell. Res. 20, 61\u2013124 (2003). https:\/\/doi.org\/10.1613\/jair.1129","journal-title":"J. Artif. Intell. Res."},{"key":"1180_CR20","unstructured":"Frank, J., Aschermann, C., Holz, T.: ETHBMC: A bounded model checker for smart contracts. In: 29th USENIX Security Symposium, pages 2757\u20132774. USENIX Association, (2020). https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/frank"},{"issue":"2","key":"1180_CR21","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/s00766-004-0191-7","volume":"9","author":"A Fuxman","year":"2004","unstructured":"Fuxman, A., Liu, L., Mylopoulos, J., Roveri, M., Traverso, P.: Specifying and analyzing early requirements in Tropos. Requir. Eng. 9(2), 132\u2013150 (2004). https:\/\/doi.org\/10.1007\/s00766-004-0191-7","journal-title":"Requir. Eng."},{"key":"1180_CR22","doi-asserted-by":"publisher","unstructured":"Goedertier, S., Vanthienen, J.: Designing compliant business processes with obligations and permissions. In: International Conference on Business Process Management, pp. 5\u201314. Springer, (2006). https:\/\/doi.org\/10.1007\/11837862_2","DOI":"10.1007\/11837862_2"},{"key":"1180_CR23","doi-asserted-by":"publisher","unstructured":"Hajdu, \u00c1., Jovanovic, D.: solc-verify: A modular verifier for Solidity smart contracts. In: Verified Software. Theories, Tools, and Experiments, VSTTE 2019, volume 12031 of LNCS, pp. 161\u2013179. Springer, (2019).https:\/\/doi.org\/10.1007\/978-3-030-41600-3_11","DOI":"10.1007\/978-3-030-41600-3_11"},{"key":"1180_CR24","unstructured":"Li, A., Long, F.: Detecting standard violation errors in smart contracts. CoRR, (2018). arxiv: 1812.07702"},{"key":"1180_CR25","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2020.103369","volume":"289","author":"J Li","year":"2020","unstructured":"Li, J., Geguang, P., Zhang, Y., Vardi, M.Y., Rozier, K.Y.: SAT-based explicit LTLf satisfiability checking. Artif. Intell. 289, 103369 (2020). https:\/\/doi.org\/10.1016\/j.artint.2020.103369","journal-title":"Artif. Intell."},{"key":"1180_CR26","doi-asserted-by":"publisher","unstructured":"Liu, Z., Liu, J.: Formal verification of blockchain smart contract based on colored petri net models. In: 2019 IEEE 43rd Annual Computer Software and Applications Conf. (COMPSAC), 2, 555\u2013560, 2019. https:\/\/doi.org\/10.1109\/COMPSAC.2019.10265","DOI":"10.1109\/COMPSAC.2019.10265"},{"key":"1180_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The temporal logic of reactive and concurrent systems - specification","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems - specification. Springer (1992). https:\/\/doi.org\/10.1007\/978-1-4612-0931-7"},{"key":"1180_CR28","doi-asserted-by":"publisher","unstructured":"Meloche, R.: Legal contract formalization in Symboleo with controlled natural language templates. Master\u2019s thesis, University of Ottawa, Canada, (2023). https:\/\/doi.org\/10.20381\/ruor-29889","DOI":"10.20381\/ruor-29889"},{"key":"1180_CR29","doi-asserted-by":"publisher","unstructured":"Montali, M.: Specification and verification of declarative open interaction models - a logic-based approach, volume 56 of LNBIP. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14538-4","DOI":"10.1007\/978-3-642-14538-4"},{"issue":"3\u20134","key":"1180_CR30","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s11334-019-00339-1","volume":"15","author":"M Narizzano","year":"2019","unstructured":"Narizzano, M., Pulina, L., Tacchella, A., Vuotto, S.: Property specification patterns at work: verification and inconsistency explanation. Innov. Syst. Softw. Eng. 15(3\u20134), 307\u2013323 (2019). https:\/\/doi.org\/10.1007\/s11334-019-00339-1","journal-title":"Innov. Syst. Softw. Eng."},{"key":"1180_CR31","doi-asserted-by":"publisher","unstructured":"Nehai, Z., Piriou, P.-Y., Daumas, F.\u00a0F.: Model-checking of smart contracts. In: 1st IEEE International Conference on Blockchain, pp. 980\u2013987. IEEE, (2018). https:\/\/doi.org\/10.1109\/Cybermatics_2018.2018.00185","DOI":"10.1109\/Cybermatics_2018.2018.00185"},{"key":"1180_CR32","doi-asserted-by":"publisher","unstructured":"Nelaturu, K., Mavridou, A., Veneris, A.\u00a0G., Laszka, A.: Verified development and deployment of multiple interacting smart contracts with veriSolid. In: IEEE International Conference on Blockchain and Cryptocurrency, ICBC 2020, pp. 1\u20139. IEEE, (2020). https:\/\/doi.org\/10.1109\/ICBC48266.2020.9169428","DOI":"10.1109\/ICBC48266.2020.9169428"},{"key":"1180_CR33","doi-asserted-by":"publisher","unstructured":"Pace, G.\u00a0J., Prisacariu, C., Schneider, G.: Model checking contracts - a case study. In: Automated Technology for Verification and Analysis, 5th International Symposium, ATVA, volume 4762 of LNCS, pp. 82\u201397. Springer, (2007). https:\/\/doi.org\/10.1007\/978-3-540-75596-8_8","DOI":"10.1007\/978-3-540-75596-8_8"},{"key":"1180_CR34","unstructured":"Parvizimosaed, A.: Symboleo: specification and verification of legal contracts. PhD thesis, Universit\u00e9 d\u2019Ottawa\/University of Ottawa, Canada, Oct. (2022). https:\/\/ruor.uottawa.ca\/handle\/10393\/44186"},{"key":"1180_CR35","doi-asserted-by":"publisher","unstructured":"Parvizimosaed, A., Sharifi, S., Amyot, D., Logrippo, L., Mylopoulos, J.: Subcontracting, assignment, and substitution for legal contracts in Symboleo. In: Conceptual Modeling, pp. 271\u2013285, Springer, Cham, (2020). https:\/\/doi.org\/10.1007\/978-3-030-62522-1_20","DOI":"10.1007\/978-3-030-62522-1_20"},{"key":"1180_CR36","doi-asserted-by":"publisher","unstructured":"Parvizimosaed, A., Roveri, M., Rasti, A., Amyot, D., Logrippo, L., Mylopoulos, J.: Model-checking legal contracts with symboleopc. In: Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems, MODELS \u201922, pp. 278\u2013288, New York, USA, (2022). ACM.https:\/\/doi.org\/10.1145\/3550355.3552449","DOI":"10.1145\/3550355.3552449"},{"issue":"6","key":"1180_CR37","doi-asserted-by":"publisher","first-page":"2395","DOI":"10.1007\/s10270-022-01053-6","volume":"21","author":"A Parvizimosaed","year":"2022","unstructured":"Parvizimosaed, A., Sharifi, S., Amyot, D., Logrippo, L., Roveri, M., Rasti, A., Roudak, A., Mylopoulos, J.: Specification and analysis of legal contracts with symboleo. Softw. Syst. Model. 21(6), 2395\u20132427 (2022). https:\/\/doi.org\/10.1007\/s10270-022-01053-6","journal-title":"Softw. Syst. Model."},{"key":"1180_CR38","unstructured":"Parvizimosaid, A., Anda, A.\u00a0A., Alfuhaid, S.: Supplementary online material, (2024). https:\/\/github.com\/Smart-Contract-Modelling-uOttawa\/Symboleo-Model-Checker-Test-Generator\/tree\/main\/Realistic_Test_algorithms\/Symboleo-Model-Checker-Test-Generator"},{"key":"1180_CR39","doi-asserted-by":"publisher","unstructured":"Pill, I., Semprini, S., Cavada, R., Roveri, M., Bloem, R., Cimatti, A.: Formal analysis of hardware requirements. In: 43rd Design Automation Conference (DAC), pp. 821\u2013826. ACM, (2006). https:\/\/doi.org\/10.1145\/1146909.1147119","DOI":"10.1145\/1146909.1147119"},{"key":"1180_CR40","doi-asserted-by":"publisher","unstructured":"Rasti, A., Amyot, D., Parvizimosaed, A., Roveri, M., Logrippo, L., Anda, A.\u00a0A., Mylopoulos, J.: Symboleo2sc: From legal contract specifications to smart contracts. In: Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems, MODELS \u201922, pp. 300\u2013310, New York, USA, (2022). ACM. https:\/\/doi.org\/10.1145\/3550355.3552407","DOI":"10.1145\/3550355.3552407"},{"key":"1180_CR41","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/j.future.2018.05.046","volume":"88","author":"A Reyna","year":"2018","unstructured":"Reyna, A., Mart\u00edn, C., Chen, J., Soler, E., D\u00edaz, M.: On blockchain and its integration with IoT, challenges and opportunities. Futur. Gener. Comput. Syst. 88, 173\u2013190 (2018). https:\/\/doi.org\/10.1016\/j.future.2018.05.046","journal-title":"Futur. Gener. Comput. Syst."},{"issue":"2","key":"1180_CR42","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10009-010-0140-3","volume":"12","author":"KY Rozier","year":"2010","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. Int. J. Softw. Tools Technol. Transf. 12(2), 123\u2013137 (2010). https:\/\/doi.org\/10.1007\/s10009-010-0140-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"1180_CR43","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s10703-019-00337-w","volume":"54","author":"C S\u00e1nchez","year":"2019","unstructured":"S\u00e1nchez, C., Schneider, G., Ahrendt, W., Bartocci, E., Bianculli, D., Colombo, C., Falcone, Y., Francalanza, A., Krstic, S., Louren\u00e7o, J.M., Nickovic, D., Pace, G.J., Rufino, J., Signoles, J., Traytel, D., Weiss, A.: A survey of challenges for runtime verification from advanced application domains (beyond software). Formal Methods Syst. Des. 54(3), 279\u2013335 (2019). https:\/\/doi.org\/10.1007\/s10703-019-00337-w","journal-title":"Formal Methods Syst. Des."},{"key":"1180_CR44","doi-asserted-by":"publisher","unstructured":"Shanahan, M.: The event calculus explained. In: Artificial Intelligence Today, pp. 409\u2013430. Springer, (1999). https:\/\/doi.org\/10.1007\/3-540-48317-9_17","DOI":"10.1007\/3-540-48317-9_17"},{"key":"1180_CR45","doi-asserted-by":"publisher","unstructured":"Sharifi, S., Parvizimosaed, A., Amyot, D., Logrippo, L., Mylopoulos, J.: Symboleo: Towards a specification language for legal contracts. In: 28th IEEE International Requirements Engineering Conference (RE 2020), pp. 364\u2013369. IEEE, (2020).https:\/\/doi.org\/10.1109\/RE48521.2020.00049","DOI":"10.1109\/RE48521.2020.00049"},{"issue":"8","key":"1180_CR46","doi-asserted-by":"publisher","first-page":"590","DOI":"10.1134\/S0361768819080164","volume":"45","author":"E Shishkin","year":"2019","unstructured":"Shishkin, E.: Debugging smart contract\u2019s business logic using symbolic model checking. Program. Comput. Softw. 45(8), 590\u2013599 (2019). https:\/\/doi.org\/10.1134\/S0361768819080164","journal-title":"Program. Comput. Softw."},{"key":"1180_CR47","doi-asserted-by":"publisher","unstructured":"Soavi, M.: From legal contracts to formal specifications. PhD thesis, Universit\u00e0 di Trento, Italy, (2022). https:\/\/doi.org\/10.15168\/11572_355741","DOI":"10.15168\/11572_355741"},{"key":"1180_CR48","doi-asserted-by":"publisher","DOI":"10.5210\/fm.v2i9.548","author":"N Szabo","year":"1997","unstructured":"Szabo, N.: Formalizing and securing relationships on public networks. First Monday (1997). https:\/\/doi.org\/10.5210\/fm.v2i9.548","journal-title":"First Monday"},{"key":"1180_CR49","unstructured":"The nuXmv team. The nuXmv symbolic model checker, (2020). https:\/\/nuxmv.fbk.eu"},{"key":"1180_CR50","doi-asserted-by":"publisher","unstructured":"van Binsbergen, L.T., Kebede, M.G., Baugh, J., van Engers, T., van Vuurden, D.G.: Dynamic generation of access control policies from social policies. Procedia. Comput. Sci. 198, 140\u2013147 (2022). https:\/\/doi.org\/10.1016\/j.procs.2021.12.221","DOI":"10.1016\/j.procs.2021.12.221"},{"key":"1180_CR51","doi-asserted-by":"publisher","unstructured":"van Binsbergen, L.T., Liu, L.-C., Van Doesburg, R., Van Engers, T.: eFLINT: a Domain-Specific Language for Executable Norm Specifications. In: 19th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE\u201920), pp. 124\u2013136. ACM, (2020). https:\/\/doi.org\/10.1145\/3425898.3426958","DOI":"10.1145\/3425898.3426958"},{"issue":"7","key":"1180_CR52","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3464421","volume":"54","author":"P Tolmach","year":"2021","unstructured":"Tolmach, P., Li, Y., Lin, S.-W., Liu, Y., Li, Z.: A survey of smart contract formal specification and verification. ACM Comput. Surv. (CSUR) 54(7), 1\u201338 (2021). https:\/\/doi.org\/10.1145\/3464421","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"1180_CR53","volume-title":"Practical model-based testing: a tools approach","author":"M Utting","year":"2010","unstructured":"Utting, M., Legeard, B.: Practical model-based testing: a tools approach. Elsevier (2010)"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01180-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-024-01180-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01180-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,24]],"date-time":"2025-07-24T07:52:35Z","timestamp":1753343555000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-024-01180-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,3]]},"references-count":53,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,8]]}},"alternative-id":["1180"],"URL":"https:\/\/doi.org\/10.1007\/s10270-024-01180-2","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2024,7,3]]},"assertion":[{"value":"13 May 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 January 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 April 2024","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 July 2024","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}