Till sidans topp

Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12

Tipsa en vän
Utskriftsversion

Modelling and analysis of… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

Modelling and analysis of normative documents

Artikel i vetenskaplig tidskrift
Författare John J. Camilleri
Gerardo Schneider
Publicerad i Journal of Logical and Algebraic Methods in Programming
Volym 91
Sidor 33-59
ISSN 2352-2208
Publiceringsår 2017
Publicerad vid Institutionen för data- och informationsteknik (GU)
Sidor 33-59
Språk en
Länkar doi.org/10.1016/j.jlamp.2017.05.002
Ämnesord contract analysis, normative documents, timed automata, Uppaal
Ämneskategorier Datavetenskap (datalogi)

Sammanfattning

We are interested in using formal methods to analyse normative documents or contracts such as terms of use, privacy policies, and service agreements. We begin by modelling such documents in terms of obligations, permissions and prohibitions of agents over actions, restricted by timing constraints and including potential penalties resulting from the non-fulfilment of clauses. This is done using the C-O Diagram formalism, which we have extended syntactically and for which we have defined a new trace semantics. Models in this formalism can then be translated into networks of timed automata, and we have a complete working implementation of this translation. The network of automata is used as a specification of a normative document, making it amenable to verification against given properties. By applying this approach to a case study from a real-world contract, we show the kinds of analysis possible through both syntactic querying on the structure of the model, as well as verification of properties using Uppaal.

Sidansvarig: Webbredaktion|Sidan uppdaterades: 2012-09-11
Dela:

På Göteborgs universitet använder vi kakor (cookies) för att webbplatsen ska fungera på ett bra sätt för dig. Genom att surfa vidare godkänner du att vi använder kakor.  Vad är kakor?