• Publication
  • PrePrints
  • Abstract - Specification and Verification of Normative Texts using C-O Diagrams
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Specification and Verification of Normative Texts using C-O Diagrams
PrePrint
ISSN: 0098-5589
Gregorio Diaz, University of Castilla-La Mancha, Albacete
María Emilia Cambronero, University of Castilla-La Mancha, Albacete
Enrique Martínez, University of Castilla-La Mancha, Albacete
Gerardo Schneider, Chalmers | University of Gothenburg, Gothenburg
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:
Modal logic,Methodologies,Specification,Representation,Formal methods,Model checking,Legal implications,Specifying and Verifying and Reasoning about Programs,Specification techniques,Temporal logic
Citation:
Gregorio Diaz, María Emilia Cambronero, Enrique Martínez, Gerardo Schneider, "Specification and Verification of Normative Texts using C-O Diagrams," IEEE Transactions on Software Engineering, 21 Nov. 2013. IEEE computer Society Digital Library. IEEE Computer Society, <http://doi.ieeecomputersociety.org/10.1109/TSE.2013.54>
Usage of this product signifies your acceptance of the Terms of Use.