{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T15:09:56Z","timestamp":1773155396991,"version":"3.50.1"},"reference-count":92,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2022,10,28]],"date-time":"2022-10-28T00:00:00Z","timestamp":1666915200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,10,28]],"date-time":"2022-10-28T00:00:00Z","timestamp":1666915200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"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"}]},{"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"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2022,12]]},"DOI":"10.1007\/s10270-022-01053-6","type":"journal-article","created":{"date-parts":[[2022,10,28]],"date-time":"2022-10-28T06:10:41Z","timestamp":1666937441000},"page":"2395-2427","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Specification and analysis of legal contracts with Symboleo"],"prefix":"10.1007","volume":"21","author":[{"given":"Alireza","family":"Parvizimosaed","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sepehr","family":"Sharifi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Amyot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luigi","family":"Logrippo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aidin","family":"Rasti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ali","family":"Roudak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Mylopoulos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,10,28]]},"reference":[{"key":"1053_CR1","unstructured":"Accord Project: Ergo. https:\/\/accordproject.org\/projects\/ergo\/ (2020)"},{"issue":"4","key":"1053_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. Commerce 12(4), 9\u201338 (2008)","journal-title":"Int. J. Electron. Commerce"},{"issue":"6","key":"1053_CR3","first-page":"1726","volume":"49","author":"MP Allard","year":"2001","unstructured":"Allard, M.P.: The retroactive effect of conditional obligations in tax law. Can. Tax J. 49(6), 1726\u20131839 (2001)","journal-title":"Can. Tax J."},{"issue":"2","key":"1053_CR4","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0004-3702(84)90008-0","volume":"23","author":"JF Allen","year":"1984","unstructured":"Allen, J.F.: Towards a general theory of action and time. Artif. Intell. 23(2), 123\u2013154 (1984)","journal-title":"Artif. Intell."},{"key":"1053_CR5","doi-asserted-by":"publisher","unstructured":"Alqahtani, S.M., He, X., Gamble, R.F., 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. ScholarSpace (2020). https:\/\/doi.org\/10.24251\/HICSS.2020.650","DOI":"10.24251\/HICSS.2020.650"},{"key":"1053_CR6","unstructured":"Alt, L.: Ethereum formal verification. https:\/\/bit.ly\/37dSc87 (2020)"},{"key":"1053_CR7","doi-asserted-by":"crossref","unstructured":"Alt, L., Reitwiessner, C.: SMT-based verification of solidity smart contracts. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, pp. 376\u2013388. Springer, Cham (2018)","DOI":"10.1007\/978-3-030-03427-6_28"},{"key":"1053_CR8","doi-asserted-by":"publisher","unstructured":"Athan, T., Boley, H., Governatori, G., Palmirani, M., Paschke, A., Wyner, A.: OASIS LegalRuleML. In: Proceedings of the Fourteenth International Conference on Artificial Intelligence and Law, ICAIL\u201913, pp. 3\u201312. ACM (2013). https:\/\/doi.org\/10.1145\/2514601.2514603","DOI":"10.1145\/2514601.2514603"},{"key":"1053_CR9","doi-asserted-by":"publisher","unstructured":"Athan, T., Governatori, G., Palmirani, M., Paschke, A., Wyner, A.: LegalRuleML: Design principles and foundations. In: Reasoning Web International Summer School, pp. 151\u2013188. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-21768-0_6","DOI":"10.1007\/978-3-319-21768-0_6"},{"issue":"3","key":"1053_CR10","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/s10506-016-9185-2","volume":"24","author":"S Azzopardi","year":"2016","unstructured":"Azzopardi, S., Pace, G.J., Schapachnik, F., Schneider, G.: Contract automata. Artif. Intell. Law 24(3), 203\u2013243 (2016). https:\/\/doi.org\/10.1007\/s10506-016-9185-2","journal-title":"Artif. Intell. Law"},{"key":"1053_CR11","unstructured":"Bettini, L.: Implementing Domain-Specific Languages with Xtext and Xtend - Second Edition. Packt Publishing (2016)"},{"key":"1053_CR12","unstructured":"Bettini, L.: Implementing domain-specific languages with Xtext and Xtend, Second edition. Packt Publishing Ltd (2016)"},{"key":"1053_CR13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139024877","volume-title":"Contract Law: Rules, Theory, and Context","author":"BH Bix","year":"2012","unstructured":"Bix, B.H.: Contract Law: Rules, Theory, and Context. Cambridge University Press, Cambridge (2012)"},{"key":"1053_CR14","unstructured":"California Independent System Operator Corporation: Appendix b.21 distributed energy resource provider agreement (2016). https:\/\/bit.ly\/2TF79rD"},{"key":"1053_CR15","doi-asserted-by":"publisher","first-page":"6735","DOI":"10.1109\/ACCESS.2017.2696577","volume":"5","author":"ME Cambronero","year":"2017","unstructured":"Cambronero, M.E., Llana, L., Pace, G.J.: A calculus supporting contract reasoning and monitoring. IEEE Access 5, 6735\u20136745 (2017). https:\/\/doi.org\/10.1109\/ACCESS.2017.2696577","journal-title":"IEEE Access"},{"key":"1053_CR16","doi-asserted-by":"crossref","unstructured":"Cardoso, H.L., Oliveira, E.: Directed deadline obligations in agent-based business contracts. In: Coordination, Organizations, Institutions and Norms in Agent Systems V, pp. 225\u2013240. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14962-7_15"},{"key":"1053_CR17","doi-asserted-by":"publisher","unstructured":"Carmo, J., Jones, A.J.I.: Deontic logic and contrary-to-duties. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol.\u00a08, pp. 265\u2013343. Springer, Dordrecht (2002). https:\/\/doi.org\/10.1007\/978-94-010-0387-2_4","DOI":"10.1007\/978-94-010-0387-2_4"},{"key":"1053_CR18","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: Biere, A., Bloem, R. (eds.) 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"},{"key":"1053_CR19","doi-asserted-by":"crossref","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: CAV 2014, LNCS, vol. 8559, pp. 334\u2013342 (2014)","DOI":"10.1007\/978-3-319-08867-9_22"},{"issue":"1","key":"1053_CR20","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)","journal-title":"Auton. Agent. Multi-Agent Syst."},{"key":"1053_CR21","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/9153.001.0001","volume-title":"Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant","author":"A Chlipala","year":"2013","unstructured":"Chlipala, A.: Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)"},{"key":"1053_CR22","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 (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29","DOI":"10.1007\/3-540-45657-0_29"},{"key":"1053_CR23","doi-asserted-by":"publisher","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\u201322:34 (2012). https:\/\/doi.org\/10.1145\/2377656.2377659","DOI":"10.1145\/2377656.2377659"},{"key":"1053_CR24","unstructured":"Clarke, E.M., Grumberg, O., Kroening, D., Peled, D.A., Veith, H.: Model Checking, 2nd Edition. MIT Press (2018)"},{"key":"1053_CR25","unstructured":"CSM Lab: Symboleo Conformance Checker (2020). https:\/\/github.com\/Smart-Contract-Modelling-uOttawa\/Symboleo-Compliance-Checker. Accessed 26 Oct 2020"},{"key":"1053_CR26","unstructured":"CSM Lab and University of Trento: Symboleo Property Checker: a nuXmv-based property checker for Symboleo specifications (2020). https:\/\/bit.ly\/3lVbao0"},{"issue":"1\u20132","key":"1053_CR27","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0167-6423(93)90021-G","volume":"20","author":"A Dardenne","year":"1993","unstructured":"Dardenne, A., Van Lamsweerde, A., Fickas, S.: Goal-directed requirements acquisition. Sci. Comput. Program. 20(1\u20132), 3\u201350 (1993)","journal-title":"Sci. Comput. Program."},{"key":"1053_CR28","doi-asserted-by":"crossref","unstructured":"Daskalopulu, A.: Modelling legal contracts as processes. In: Database and Expert Systems Applications, 2000. 11th International Workshop on, pp. 1074\u20131079. IEEE (2000)","DOI":"10.1109\/DEXA.2000.875160"},{"key":"1053_CR29","unstructured":"Daskalopulu, A.K.: Logic-based tools for the analysis and representation of legal contracts. Ph.D. thesis, Citeseer (1999)"},{"key":"1053_CR30","unstructured":"Digital Asset Holdings: DAML. https:\/\/daml.com\/ (2020)"},{"key":"1053_CR31","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"issue":"2","key":"1053_CR32","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1109\/MIS.2015.6","volume":"30","author":"W El Kholy","year":"2015","unstructured":"El Kholy, W., El-Menshawy, M., Bentahar, J., Qu, H., Dssouli, R.: Formal specification and automatic verification of conditional commitments. IEEE Intell. Syst. 30(2), 36\u201344 (2015)","journal-title":"IEEE Intell. Syst."},{"issue":"3","key":"1053_CR33","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/s10458-012-9208-7","volume":"27","author":"M El Menshawy","year":"2013","unstructured":"El Menshawy, M., Bentahar, J., El Kholy, W., Dssouli, R.: Reducing model checking commitments for agent communication to model checking ARCTL and GCTL. Auton. Agent. Multi-Agent Syst. 27(3), 375\u2013418 (2013)","journal-title":"Auton. Agent. Multi-Agent Syst."},{"key":"1053_CR34","unstructured":"El\u00a0Menshawy, M., Bentahar, J., Qu, H., Dssouli, R.: On the verification of social commitments and time. In: The 10th International Conference on Autonomous Agents and Multiagent Systems-Volume 2, pp. 483\u2013490 (2011)"},{"issue":"3","key":"1053_CR35","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":"1053_CR36","unstructured":"Ethereum Foundation: Solidity. https:\/\/solidity.readthedocs.io\/ (2020)"},{"key":"1053_CR37","doi-asserted-by":"crossref","unstructured":"Farmer, W.M., Hu, Q.: FCL: a formal language for writing contracts. In: Quality Software Through Reuse and Integration, pp. 190\u2013208. Springer (2016)","DOI":"10.1007\/978-3-319-56157-8_9"},{"key":"1053_CR38","doi-asserted-by":"crossref","unstructured":"Farrell, A.D., Sergot, M.J., Sall\u00e9, M., Bartolini, C., Trastour, D., Christodoulou, A.: Performance monitoring of service-level agreements for utility computing using the event calculus. In: Electronic Contracting, 2004. Proceedings. First IEEE International Workshop on, pp. 17\u201324. IEEE (2004)","DOI":"10.1109\/WEC.2004.1319504"},{"issue":"2","key":"1053_CR39","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":"1053_CR40","doi-asserted-by":"crossref","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)","DOI":"10.1007\/11837862_2"},{"key":"1053_CR41","doi-asserted-by":"crossref","unstructured":"Governatori, G.: Representing business contracts in RuleML. Int. J. Cooperative Inf. Syst. 14(02n03), 181\u2013216 (2005)","DOI":"10.1142\/S0218843005001092"},{"issue":"4","key":"1053_CR42","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/s10506-018-9223-3","volume":"26","author":"G Governatori","year":"2018","unstructured":"Governatori, G., Idelberger, F., Milosevic, Z., Riveret, R., Sartor, G., Xu, X.: On legal contracts, imperative and declarative smart contracts, and blockchain systems. Artif. Intell. Law 26(4), 377\u2013409 (2018)","journal-title":"Artif. Intell. Law"},{"key":"1053_CR43","unstructured":"Governatori, G., Milosevic, Z.: Dealing with contract violations: formalism and domain specific language. In: EDOC Enterprise Computing Conference, 2005 Ninth IEEE International, pp. 46\u201357. IEEE (2005)"},{"issue":"04","key":"1053_CR44","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1142\/S0218843006001529","volume":"15","author":"G Governatori","year":"2006","unstructured":"Governatori, G., Milosevic, Z.: A formal analysis of a business contract language. Int. J. Cooperative Inf. Syst. 15(04), 659\u2013685 (2006)","journal-title":"Int. J. Cooperative Inf. Syst."},{"key":"1053_CR45","unstructured":"Greenspan, S.J., Mylopoulos, J., Borgida, A.: Capturing more world knowledge in the requirements specification. In: Proceedings of the 6th International Conference on Software Engineering, pp. 225\u2013234 (1982)"},{"key":"1053_CR46","unstructured":"Griffo, C., Almeida, J.P.A., Guizzardi, G.: Towards a legal core ontology based on Alexy\u2019s theory of fundamental rights. In: Multilingual Workshop on Artificial Intelligence and Law (ICAIL) (2015)"},{"key":"1053_CR47","doi-asserted-by":"crossref","unstructured":"Griffo, C., Almeida, J.P.A., Guizzardi, G., Nardi, J.C.: From an ontology of service contracts to contract modeling in enterprise architecture. In: 2017 IEEE 21st International Enterprise Distributed Object Computing Conference (EDOC), pp. 40\u201349. IEEE (2017)","DOI":"10.1109\/EDOC.2017.15"},{"issue":"3\u20134","key":"1053_CR48","doi-asserted-by":"publisher","first-page":"259","DOI":"10.3233\/AO-150157","volume":"10","author":"G Guizzardi","year":"2015","unstructured":"Guizzardi, G., Wagner, G., Almeida, J.P.A., Guizzardi, R.S.: Towards ontological foundations for conceptual modeling: the unified foundational ontology (UFO) story. Appl. Ontol. 10(3\u20134), 259\u2013271 (2015)","journal-title":"Appl. Ontol."},{"key":"1053_CR49","doi-asserted-by":"crossref","unstructured":"Hashmi, M., Governatori, G., Wynn, M.T.: Modeling obligations with event-calculus. In: International Workshop on Rules and Rule Markup Languages for the Semantic Web, LNCS, vol. 8620, pp. 296\u2013310. Springer (2014)","DOI":"10.1007\/978-3-319-09870-8_22"},{"key":"1053_CR50","doi-asserted-by":"publisher","first-page":"16","DOI":"10.2307\/785533","volume":"23","author":"WN Hohfeld","year":"1913","unstructured":"Hohfeld, W.N.: Some fundamental legal conceptions as applied in judicial reasoning. Yale Lj 23, 16 (1913)","journal-title":"Yale Lj"},{"issue":"3","key":"1053_CR51","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1093\/jigpal\/4.3.427","volume":"4","author":"AJ Jones","year":"1996","unstructured":"Jones, A.J., Sergot, M.: A formal characterisation of institutionalised power. Logic J. IGPL 4(3), 427\u2013443 (1996)","journal-title":"Logic J. IGPL"},{"issue":"268\u2013272","key":"1053_CR52","first-page":"30","volume":"53","author":"E Kindler","year":"1994","unstructured":"Kindler, E.: Safety and liveness properties: a survey. Bull. Eur. Assoc. Theor. Comput. Sci. 53(268\u2013272), 30 (1994)","journal-title":"Bull. Eur. Assoc. Theor. Comput. Sci."},{"key":"1053_CR53","doi-asserted-by":"publisher","first-page":"317","DOI":"10.26686\/vuwlr.v31i2.5956","volume":"31","author":"J Kirby","year":"2000","unstructured":"Kirby, J.: Assignments and transfers of contractual duties: Integrating theory and practice. Victoria U. Wellington L. Rev. 31, 317 (2000)","journal-title":"Victoria U. Wellington L. Rev."},{"key":"1053_CR54","doi-asserted-by":"crossref","unstructured":"Kowalski, R.A., Sergot, M.J.: A logic-based calculus of events. In: Schmidt, J.W., Thanos, C. (eds.) Foundations of Knowledge Base Management: Contributions from Logic, Databases, and Artificial Intelligence, Book resulting from the Xania Workshop 1985, Topics in Information Systems, pp. 23\u201355. Springer, Berlin (1985)","DOI":"10.1007\/978-3-642-83397-7_2"},{"key":"1053_CR55","doi-asserted-by":"crossref","unstructured":"Ladleif, J., Weske, M.: A unifying model of legal smart contracts. In: Conceptual Modeling, pp. 323\u2013337. Springer, Cham (2019)","DOI":"10.1007\/978-3-030-33223-5_27"},{"issue":"1","key":"1053_CR56","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0167-9236(88)90096-6","volume":"4","author":"RM Lee","year":"1988","unstructured":"Lee, R.M.: A logic model for electronic contracting. Decis. Support Syst. 4(1), 27\u201344 (1988)","journal-title":"Decis. Support Syst."},{"key":"1053_CR57","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2021.102665","volume":"208","author":"TC Lethbridge","year":"2021","unstructured":"Lethbridge, T.C., Forward, A., Badreddin, O., Brestovansky, D., Garzon, M., Aljamaan, H., Eid, S., Husseini Orabi, A., Husseini Orabi, M., Abdelzad, V., Adesina, O., Alghamdi, A., Algablan, A., Zakariapour, A.: Umple: model-driven development for open source and education. Sci. Comput. Program. 208, 102665 (2021). https:\/\/doi.org\/10.1016\/j.scico.2021.102665","journal-title":"Sci. Comput. Program."},{"key":"1053_CR58","doi-asserted-by":"crossref","unstructured":"Letia, I.A., Groza, A.: Running contracts with defeasible commitment. In: International Conference on Industrial, Engineering and Other Applications of Applied Intelligent Systems, LNCS, vol. 4031, pp. 91\u2013100. Springer (2006)","DOI":"10.1007\/11779568_12"},{"key":"1053_CR59","doi-asserted-by":"publisher","first-page":"1","DOI":"10.17351\/ests2017.107","volume":"3","author":"KE Levy","year":"2017","unstructured":"Levy, K.E.: Book-smart, not street-smart: blockchain-based smart contracts and the social workings of law. Engag. Sci. Technol. Soc. 3, 1\u201315 (2017)","journal-title":"Engag. Sci. Technol. Soc."},{"key":"1053_CR60","doi-asserted-by":"publisher","unstructured":"Lloyd, J.W.: Foundations of Logic Programming, 2nd Edition. Springer (1987). https:\/\/doi.org\/10.1007\/978-3-642-83189-8","DOI":"10.1007\/978-3-642-83189-8"},{"issue":"1","key":"1053_CR61","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10009-015-0378-x","volume":"19","author":"A Lomuscio","year":"2017","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transf. 19(1), 9\u201330 (2017). https:\/\/doi.org\/10.1007\/s10009-015-0378-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1053_CR62","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","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","journal-title":"Springer"},{"key":"1053_CR63","unstructured":"Meyer, J.J.C.: Deontic logic: A concise overview. In: Deontic Logic in Computer Science: Normative System Specification, pp. 3\u201316. Wiley (1993)"},{"issue":"2","key":"1053_CR64","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1080\/17579961.2017.1378468","volume":"9","author":"E Mik","year":"2017","unstructured":"Mik, E.: Smart contracts: terminology, technical limitations and real world complexity. Law Innov. Technol. 9(2), 269\u2013300 (2017)","journal-title":"Law Innov. Technol."},{"key":"1053_CR65","unstructured":"Montali, M.: jREC. https:\/\/www.inf.unibz.it\/~montali\/tools.html (2016)"},{"issue":"16","key":"1053_CR66","doi-asserted-by":"publisher","first-page":"i227","DOI":"10.1093\/bioinformatics\/btn275","volume":"24","author":"PT Monteiro","year":"2008","unstructured":"Monteiro, P.T., Ropers, D., Mateescu, R., Freitas, A.T., De Jong, H.: Temporal logic patterns for querying dynamic models of cellular interaction networks. Bioinformatics 24(16), i227\u2013i233 (2008)","journal-title":"Bioinformatics"},{"key":"1053_CR67","doi-asserted-by":"publisher","unstructured":"Nehai, Z., Piriou, P., Daumas, F.F.: Model-checking of smart contracts. In: IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData), pp. 980\u2013987. IEEE (2018). https:\/\/doi.org\/10.1109\/Cybermatics_2018.2018.00185","DOI":"10.1109\/Cybermatics_2018.2018.00185"},{"key":"1053_CR68","doi-asserted-by":"publisher","unstructured":"Nelaturu, K., Mavridou, A., Veneris, A.G., 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":"1053_CR69","unstructured":"OMG: Unified modeling language (omg uml), version 2.5.1. https:\/\/www.omg.org\/spec\/UML\/ (2017)"},{"key":"1053_CR70","doi-asserted-by":"publisher","unstructured":"Pace, G.J., Prisacariu, C., Schneider, G.: Model checking contracts: a case study. In: Automated Technology for Verification and Analysis, 5th International Symposium, ATVA, LNCS, vol. 4762, pp. 82\u201397. Springer, Berlin (2007). https:\/\/doi.org\/10.1007\/978-3-540-75596-8_8","DOI":"10.1007\/978-3-540-75596-8_8"},{"key":"1053_CR71","doi-asserted-by":"publisher","unstructured":"Parvizimosaed, A., Sharifi, S.: Symboleo Compliance Checker, v0.2 (2020). https:\/\/doi.org\/10.5281\/zenodo.3840727","DOI":"10.5281\/zenodo.3840727"},{"key":"1053_CR72","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 (ER 2020), pp. 271\u2013285. Springer International Publishing, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-62522-1_20","DOI":"10.1007\/978-3-030-62522-1_20"},{"key":"1053_CR73","doi-asserted-by":"crossref","unstructured":"Permenev, A., Dimitrov, D., Tsankov, P., Drachsler-Cohen, D., Vechev, M.: Verx: safety verification of smart contracts. In: 2020 IEEE Symposium on Security and Privacy, SP, pp. 18\u201320 (2020)","DOI":"10.1109\/SP40000.2020.00024"},{"key":"1053_CR74","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"},{"issue":"1","key":"1053_CR75","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF00370671","volume":"57","author":"H Prakken","year":"1996","unstructured":"Prakken, H., Sergot, M.: Contrary-to-duty obligations. Stud. Logica. 57(1), 91\u2013115 (1996)","journal-title":"Stud. Logica."},{"key":"1053_CR76","doi-asserted-by":"crossref","unstructured":"Prisacariu, C., Schneider, G.: A formal language for electronic contracts. In: International Conference on Formal Methods for Open Object-Based Distributed Systems, pp. 174\u2013189. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-72952-5_11"},{"key":"1053_CR77","doi-asserted-by":"publisher","unstructured":"Reyna, A., Mart\u00edn, C., Chen, J., Soler, E., D\u00edaz, M.: On blockchain and its integration with IoT. challenges and opportunities. Future Gener. Comput. Syst. 88, 173\u2013190 (2018). https:\/\/doi.org\/10.1016\/j.future.2018.05.046","DOI":"10.1016\/j.future.2018.05.046"},{"key":"1053_CR78","doi-asserted-by":"crossref","unstructured":"Shanahan, M.: The event calculus explained. In: Artificial intelligence today, pp. 409\u2013430. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48317-9_17"},{"key":"1053_CR79","doi-asserted-by":"publisher","unstructured":"Sharifi, S.: Smart contracts: From formal specification to blockchain code. Master\u2019s thesis, University of Ottawa, Canada (2020). https:\/\/doi.org\/10.20381\/ruor-25092","DOI":"10.20381\/ruor-25092"},{"key":"1053_CR80","doi-asserted-by":"publisher","unstructured":"Sharifi, S., Parvizimosaed, A.: Symboleo Text Editor, v0.1 (2020). https:\/\/doi.org\/10.5281\/zenodo.3840773","DOI":"10.5281\/zenodo.3840773"},{"key":"1053_CR81","doi-asserted-by":"publisher","unstructured":"Sharifi, S., Parvizimosaed, A., Amyot, D., Logrippo, L., Mylopoulos, J.: Symboleo: A specification language for smart contracts. In: 28th IEEE International Requirements Engineering Conference (RE\u201920), pp. 384\u2013389. IEEE CS (2020). https:\/\/doi.org\/10.1109\/RE48521.2020.00049","DOI":"10.1109\/RE48521.2020.00049"},{"issue":"3","key":"1053_CR82","doi-asserted-by":"publisher","first-page":"3454","DOI":"10.1109\/JSYST.2019.2903172","volume":"13","author":"P Siano","year":"2019","unstructured":"Siano, P., De Marco, G., Rol\u00e1n, A., Loia, V.: A survey and evaluation of the potentials of distributed ledger technology for peer-to-peer transactive energy exchanges in local energy markets. IEEE Syst. J. 13(3), 3454\u20133466 (2019). https:\/\/doi.org\/10.1109\/JSYST.2019.2903172","journal-title":"IEEE Syst. J."},{"key":"1053_CR83","doi-asserted-by":"crossref","unstructured":"Soavi, M., Zeni, N., Mylopoulos, J., Mich, L.: Contratto\u2013a method for transforming legal contracts into formal specifications. In: 16th International Conference on Research Challenges in Information Science (RCIS\u201922). Springer, Berlin (2022)","DOI":"10.1007\/978-3-031-05760-1_20"},{"issue":"17","key":"1053_CR84","doi-asserted-by":"publisher","DOI":"10.1002\/dac.3808","volume":"31","author":"A Souri","year":"2018","unstructured":"Souri, A., Rahmani, A.M., Jafari Navimipour, N.: Formal verification approaches in the web service composition: a comprehensive analysis of the current challenges for future research. Int. J. Commun Syst 31(17), e3808 (2018). https:\/\/doi.org\/10.1002\/dac.3808","journal-title":"Int. J. Commun Syst"},{"key":"1053_CR85","unstructured":"Steinberg, D., Budinsky, F., Merks, E., Paternostro, M.: EMF: Eclipse Modeling Framework. Pearson Education (2008)"},{"key":"1053_CR86","doi-asserted-by":"crossref","unstructured":"Szabo, N.: Formalizing and securing relationships on public networks. First Monday 2(9) (1997)","DOI":"10.5210\/fm.v2i9.548"},{"key":"1053_CR87","unstructured":"The British Standards Institution: PAS 333, smart legal contracts - specification (2020). https:\/\/accordproject.org\/news\/bsi\/. Online; Accessed 26 Oct 2020"},{"key":"1053_CR88","unstructured":"The nuXmv team: The nuXmv symbolic model checker (2020). https:\/\/nuxmv.fbk.eu"},{"key":"1053_CR89","doi-asserted-by":"publisher","unstructured":"Thomas Van Binsbergen, L., 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). ACM (2020). https:\/\/doi.org\/10.1145\/3425898.3426958","DOI":"10.1145\/3425898.3426958"},{"key":"1053_CR90","unstructured":"Tikhomirov, S.: Smart Contract Languages. https:\/\/github.com\/s-tikhomirov\/smart-contract-languages (2020). [Online; accessed 23-April-2020]"},{"key":"1053_CR91","unstructured":"Tolmach, P., Li, Y., Lin, S.W., Liu, Y., Li, Z.: A survey of smart contract formal specification and verification (2020). arXiv:2008.02712"},{"key":"1053_CR92","unstructured":"Wikipedia contributors: Asset \u2014 Wikipedia, the free encyclopedia. https:\/\/bit.ly\/35TjZrn (2019). [Online; accessed 21-October-2019]"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-022-01053-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-022-01053-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-022-01053-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,6]],"date-time":"2024-10-06T19:01:27Z","timestamp":1728241287000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-022-01053-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,28]]},"references-count":92,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["1053"],"URL":"https:\/\/doi.org\/10.1007\/s10270-022-01053-6","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,28]]},"assertion":[{"value":"2 November 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 September 2022","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 September 2022","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 October 2022","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}