The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.08 - Aug. (2014 vol.40)
pp: 795-817
Gerardo Schneider , Dept. of Comput. Sci. & Eng., Chalmers Univ. of Gothenburg, Gothenburg, Sweden
ABSTRACT
C-O diagrams have been introduced as a means to have a more visual representation of normative texts and electronic contracts, where it is possible to represent the obligations, permissions and prohibitions of the different signatories, as well as the penalties resulting from non-fulfillment of their obligations and prohibitions. In such diagrams we are also able to represent absolute and relative timing constraints. In this paper we present a formal semantics for C-O diagrams based on timed automata extended with information regarding the satisfaction and violation of clauses in order to represent different deontic modalities. As a proof of concept, we apply our approach to two different case studies, where the method presented here has successfully identified problems in the specification.
INDEX TERMS
Automata, Clocks, Contracts, Semantics, Cost accounting, Synchronization, Formal languages,C-O diagrams, Normative documents, electronic contracts, deontic logic, formal verification, visual models, timed automata
CITATION
Gerardo Schneider, "Specification and Verification of Normative Texts Using C-O Diagrams", IEEE Transactions on Software Engineering, vol.40, no. 8, pp. 795-817, Aug. 2014, doi:10.1109/TSE.2013.54
68 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool