Prolog-Resoner

Symboleo Compliance Checker

This tool is a compliance checker for formal contract specifications written in Symboleo. It was inspired by the tool jREC. It evaluates whether given sequences of events (i.e., traces) are compliant with given contract specifications. To this aim, the tool supports Symboleo's primitive predicates (such as within and occur), axiomatized semantics, description of contracts, and compliance scenarios. For each contract specification, we have a part consisting of reusable, domain-independent axioms and a contract-specific part, both written in Prolog. The reusable axioms are replicated in each contract. They formalize the state machines of norms. The contract-specific part describes the list of parameterized obligations and powers that is specific to each contract. Symboleo proposes templates for contracts, obligations, powers, and events.

The tool and detailed information is available in our GitHub.