SymboleoPC: checking properties of legal contracts

Legal contracts specify requirements for business transactions. SYMBOLEO was recently proposed as a formal specification language for legal contracts. It allows the specification of the contractual requirements by specifying the obligations and powers of the parties, as well as specifying the events that can occur in a contract's lifecycle. With appropriate tool support, SYMBOLEO can allow monitoring the contract lifecycle. However, because of mistakes in contract interpretation or formal specification, specified contracts may violate properties expected by contracting parties. This paper presents SYMBOLEOPC, a tool for analyzing SYMBOLEO contracts using the NUXMV model checker, where properties can be expressed in both Linear Temporal Logic and Computation Tree Logic. The presentation highlights the architecture, implementation, and testing of the tool, as well as a scalability evaluation, based on performance data. The performance of the tool was evaluated with respect to varying numbers of obligations and powers, with varying numbers of inter-dependencies among them, with parameters derived from the analysis of real contracts. These results suggest that SYMBOLEOPC can be usefully applied to the analysis of formal specifications of contracts with real-life sizes and structures.