Legal contracts specify the terms and conditions—in essence, requirements—that apply to business transactions. This paper proposes a formal specification language for legal contracts, called Symboleo, where contracts consist of collections of obligations and powers that define a legal contract’s compliant executions. Symboleo offers execution time operations such as subcontracting, assignment, and substitution. Its formal semantics is defined in terms of logical axioms on statecharts that describe the lifetimes of contracts, obligations, and powers. We have implemented two tools to support the analysis of contract specifications. One is a conformance validation tool that enables checking that a specification is consistent with the expectations of contracting parties. The other tool enables model-checking of desired contract properties, expressed in temporal logic. We envision Symboleo with its associated tools as enablers for the formal verification of contracts to detect requirements-level issues. Our proposal includes an evaluation through the specification of two real life-inspired contracts.

Specification and analysis of legal contracts with Symboleo / Parvizimosaed, A.; Sharifi, S.; Amyot, D.; Logrippo, L.; Roveri, M.; Rasti, A.; Roudak, A.; Mylopoulos, J.. - In: SOFTWARE AND SYSTEMS MODELING. - ISSN 1619-1366. - 21:6(2022), pp. 2395-2427. [10.1007/s10270-022-01053-6]

Specification and analysis of legal contracts with Symboleo

Roveri M.;Mylopoulos J.
2022-01-01

Abstract

Legal contracts specify the terms and conditions—in essence, requirements—that apply to business transactions. This paper proposes a formal specification language for legal contracts, called Symboleo, where contracts consist of collections of obligations and powers that define a legal contract’s compliant executions. Symboleo offers execution time operations such as subcontracting, assignment, and substitution. Its formal semantics is defined in terms of logical axioms on statecharts that describe the lifetimes of contracts, obligations, and powers. We have implemented two tools to support the analysis of contract specifications. One is a conformance validation tool that enables checking that a specification is consistent with the expectations of contracting parties. The other tool enables model-checking of desired contract properties, expressed in temporal logic. We envision Symboleo with its associated tools as enablers for the formal verification of contracts to detect requirements-level issues. Our proposal includes an evaluation through the specification of two real life-inspired contracts.
2022
6
Parvizimosaed, A.; Sharifi, S.; Amyot, D.; Logrippo, L.; Roveri, M.; Rasti, A.; Roudak, A.; Mylopoulos, J.
Specification and analysis of legal contracts with Symboleo / Parvizimosaed, A.; Sharifi, S.; Amyot, D.; Logrippo, L.; Roveri, M.; Rasti, A.; Roudak, A.; Mylopoulos, J.. - In: SOFTWARE AND SYSTEMS MODELING. - ISSN 1619-1366. - 21:6(2022), pp. 2395-2427. [10.1007/s10270-022-01053-6]
File in questo prodotto:
File Dimensione Formato  
s10270-022-01053-6.pdf

Solo gestori archivio

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 4.06 MB
Formato Adobe PDF
4.06 MB Adobe PDF   Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/364826
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 3
social impact