| 1. |
- Camilleri, John J., 1986, et al.
(author)
-
Modelling and analysis of normative documents
- 2017
-
In: Journal of Logical and Algebraic Methods in Programming. - : Elsevier BV. - 2352-2208 .- 2352-2216. ; 91, s. 33-59
-
Journal article (peer-reviewed)abstract
- 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.
|
|
| 2. |
|
|
| 3. |
|
|
| 4. |
|
|
| 5. |
- Pardo Jimenez, Raul, 1988, et al.
(author)
-
Formalising privacy policies in social networks
- 2017
-
In: Journal of Logical and Algebraic Methods in Programming. - : Elsevier BV. - 2352-2208 .- 2352-2216. ; 90, s. 125-157
-
Journal article (peer-reviewed)abstract
- Social Network Services (SNS) have changed the way people communicate, bringing many benefits but also new concerns. Privacy is one of them. We present a framework to write privacy policies for SNSs and to reason about such policies in the presence of events making the network evolve. The framework includes a model of SNSs, a logic to specify properties and to reason about the knowledge of the users (agents) of the SNS, and a formal language to write privacy policies. Agents are enhanced with a reasoning engine allowing the inference of knowledge from previously acquired knowledge. To describe the way SNSs may evolve, we provide operational semantics rules which are classified into four categories: epistemic, topological, policy, and hybrid, depending on whether the events under consideration change the knowledge of the SNS' users, the structure of the social graph, the privacy policies, or a combination of the above, respectively. We provide specific rules for describing Twitter's behaviour, and prove that it is privacy-preserving (i.e., that privacy is preserved under every possible event of the system). We also show how Twitter and Facebook are not privacy-preserving in the presence of additional natural privacy policies. (C) 2017 Elsevier Inc. All rights reserved.
|
|
| 6. |
- Emilio, Tuosto, et al.
(author)
-
Semantics of global view of choreographies
- 2017
-
In: Journal of Logic and Algebraic Programming. - : Elsevier BV. - 1567-8326 .- 1873-5940 .- 2352-2208. ; 95
-
Journal article (peer-reviewed)abstract
- We propose two abstract semantics of the global view of choreographies given in terms of partial orders. The first semantics is formalised as pomsets of communication events while the second one is based on hypergraphs of events. These semantics can accommodate different levels of abstractions. We discuss the adequacy of our models by considering their relation with communicating machines, that we use to formalise the local view. Our approach increases expressiveness and allows us to overcome some limitations that affect alternative semantics of global views. This will be illustrated by discussing some interesting examples. Finally, we show that the two semantics are equivalent and have different merits. More precisely, the semantics based on pomsets yields a more elegant presentation, but it is less suitable for implementation. The semantics based on hypergraphs instead is amenable to a straightforward implementation.
|
|
