| Summary: | O conceito de contrato desempenha um papel importante no mundo dos negócios em que relações comerciais entre diferentes partes são ditadas por normas legais. Esse método de negociação tem sido cada vez mais utilizado por meio de transações eletrônicas, devido aos avanços tecnológicos e à globalização. Com isso, algumas dificuldades surgiram para se garantir a confiabilidade entre as partes interessadas na realização das negociações. Uma forma de se garantir propriedades e acordos em contratos eletrônicos é verificação automática e rigorosa com base em formalismos matemáticos. Alguns formalismos, como as lógicas de ôntica e dinâmica, são empregados na representação de contratos eletrônicos. Modelos formais com suporte computacional permitem alcançar resultados mais precisos na verificação desses contratos. Em decorrência de tal êxito, estudos sobre contratos eletrônicos têm sido amplamente abordados na literatura. No entanto, novos desafios surgem nesse contexto, como por exemplo, a detecção de conflitos em contratos multilaterais, porém, poucos trabalhos têm lidado com essa forma contratual. Devido a isso, este trabalho propõe uma forma de representar adequadamente os contratos multilaterais por meio de formalismos e verificar automaticamente propriedades em contratos dessa natureza. Neste sentido, o trabalho apresenta a ferramenta RECALL um verificador automático para detecção de conflitos em contratos multilaterais. Além disso, um estudo de caso real de venda de produtos via Internet, caracterizado por aspectos multilaterais, é modelado e verificado usando a ferramenta RECALL. Com a aplicacão prática no contrato de vendas é possível fornecer uma prova de conceito sobre as funcionalidades da ferramenta desenvolvida. === The notion of contracts has played an important role in business where trade relationships between different parties are dictated by legal rules. This concept has been used increasingly by electronic transactions due to technological advances and globalization. Therefore, new challenges have emerged to guarantee the reliability among stakeholders in electronic negotiations. Automatic verification based on formalisms lays the foundations to guarantee properties and agreements on electronic contracts. Some formalisms, such as deontic and dynamic logics, are used to represent electronic contracts. Formal models and computational support allow to attain more precise results on checking electronic contracts. The automatic verification of electronic contracts has arisen as a new challenge especially in the task of detecting conflicts in multi-party contracts. The problem of checking contracts has been largely addressed in the literature, but only few works have dealt with multi-party ones. This work proposes an approach to represent appropriately multi-party contracts by means of suitable formalisms and also to automatically verify properties in contracts of this nature. We present the RECALL tool, an automatic checker for finding conflicts on multi-party contracts. A real world case study characterized by multilateral aspects is also modeled and verified using the RECALL tool. Further, the practical application of our tool in a real world problem provides a proof of concept upon their functionalities.
|
|---|
