| 1. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Tree Regular Model Checking : A simulation-based approach
- 2006
-
Ingår i: Journal of Logic and Algebraic Programming. - : Elsevier BV. - 1567-8326 .- 1873-5940. ; 69:1-2, s. 93-121
-
Tidskriftsartikel (refereegranskat)abstract
- Regular model checking is the name of a family of techniques for analyzing infinite-state systems in which states are represented by words, sets of states by finite automata, and transitions by finite-state transducers. In this framework, the central problem is to compute the transitive closure of a transducer. Such a representation allows to compute the set of reachable states of the system and to detect loops between states. A main obstacle of this approach is that there exists many systems for which the reachable set of states is not regular. Recently, regular model checking has been extended to systems with tree-like architectures. In this paper, we provide a procedure, based on a new implementable acceleration technique, for computing the transitive closure of a tree transducer. The procedure consists of incrementally adding new transitions while merging states, which are related according to a pre-defined equivalence relation. The equivalence is induced by a downward and an upward simulation relation, which can be efficiently computed. Our technique can also be used to compute the set of reachable states without computing the transitive closure. We have implemented and applied our technique to various protocols.
|
|
| 2. |
- Aktug, Irem, et al.
(författare)
-
Provably Correct Runtime Monitoring
- 2009
-
Ingår i: Journal of Logic and Algebraic Programming. - : Elsevier BV. - 1567-8326 .- 1873-5940. ; 78:5, s. 304-339
-
Tidskriftsartikel (refereegranskat)abstract
- Runtime monitoring is an established technique to enforce a wide range of program safety and security properties. We present a formalization of monitoring and monitor inlining, for the Java Virtual Machine. Monitors are security automata given in a special-purpose monitor specification language, ConSpec. The automata operate on finite or infinite strings of calls to a fixed API, allowing local dependencies on parameter values and heap content. We use a two-level class file annotation scheme to characterize two key properties: (i) that the program is correct with respect to the monitor as a constraint on allowed program behavior, and (ii) that the program has a copy of the given monitor embedded into it. As the main application of these results we sketch a simple inlining algorithm and show how the two-level annotations can be completed to produce a fully annotated program which is valid in the standard sense of Floyd/Hoare logic. This establishes the mediation property that inlined programs are guaranteed to adhere to the intended policy. Furthermore, validity can be checked efficiently using a weakest precondition based annotation checker, thus preparing the ground for on-device checking of policy adherence in a proof-carrying code setting.
|
|
| 3. |
- Angelov, Krasimir, 1978, et al.
(författare)
-
A Framework for Conflict Analysis of Normative Texts Written in Controlled Natural Language
- 2013
-
Ingår i: Journal of Logic and Algebraic Programming. - : Elsevier BV. - 1567-8326. ; 82:5-7, s. 216-240
-
Tidskriftsartikel (refereegranskat)abstract
- In this paper we are concerned with the analysis of normative conflicts, or the detection of conflicting obligations, permissions and prohibitions in normative texts written in a Controlled Natural Language (CNL). For this we present AnaCon, a proof-of-concept system where normative texts written in CNL are automatically translated into the formal language CL using the Grammatical Framework (GF). Such CL expressions are then analysed for normative conflicts by the CLAN tool, which gives counter-examples in cases where conflicts are found. The framework also uses GF to give a CNL version of the counter-example, helping the user to identify the conflicts in the original text. We detail the application of AnaCon to two case studies and discuss the effectiveness of our approach.
|
|
| 4. |
|
|
| 5. |
- Emilio, Tuosto, et al.
(författare)
-
Semantics of global view of choreographies
- 2017
-
Ingår i: Journal of Logic and Algebraic Programming. - : Elsevier BV. - 1567-8326 .- 1873-5940 .- 2352-2208. ; 95
-
Tidskriftsartikel (refereegranskat)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.
|
|
| 6. |
- Johansson, Magnus, et al.
(författare)
-
Computing Strong and Weak Bisimulations for Psi-Calculi
- 2012
-
Ingår i: Journal of Logic and Algebraic Programming. - : Elsevier. - 1567-8326 .- 1873-5940. ; 81:3, s. 162-180
-
Tidskriftsartikel (refereegranskat)abstract
- We present a symbolic transition system and strong and weak bisimulation equivalences for psi-calculi, and show that they are fully abstract with respect to bisimulation congruences in the non-symbolic semantics. A procedure which computes the most general constraint under which two agents are bisimilar is developed and proved correct. A psi-calculus is an extension of the pi-calculus with nominal data types for data structures and for logical assertions representing facts about data. These can be transmitted between processes and their names can be statically scoped using the standard pi-calculus mechanism to allow for scope migrations. Psi-calculi can be more general than other proposed extensions of the pi-calculus such as the applied pi-calculus, the spi-calculus, the fusion calculus, or the concurrent constraint pi-calculus. Symbolic semantics are necessary for an efficient implementation of the calculus in automated tools exploring state spaces, and the full abstraction property means the symbolic semantics makes exactly the same distinctions as the original.
|
|
| 7. |
|
|
| 8. |
- Prisacariu, C., et al.
(författare)
-
A dynamic deontic logic for complex contracts
- 2012
-
Ingår i: Journal of Logic and Algebraic Programming. - : Elsevier BV. - 1567-8326. ; 81:4, s. 458-490
-
Tidskriftsartikel (refereegranskat)abstract
- We present a dynamic deontic logic for specifying and reasoning about complex contracts. The concepts that our contract logic CL. captures are drawn from legal contracts, as we consider that these are more general and expressive than what is usually found in computer science (like in software contracts, web services specifications, or communication protocols). CL is intended to be used in specifying complex contracts found in computer science. This influences many of the design decisions behind CL. We adopt an ought-to-do approach to deontic logic and apply the deontic modalities exclusively over complex actions. On top, we add the modalities of dynamic logic so to be able to reason about what happens after an action is performed. CL can reason about regular synchronous actions capturing the notion of actions done at the same time. CL incorporates the notions of contrary-to-duty and contrary-to-prohibition by attaching to the deontic modalities explicitly a reparation which is to be enforced in case of violations. Results of decidability and tree model property are given as well as specific properties for the modalities. (C) 2012 Elsevier Inc. All rights reserved.
|
|
| 9. |
- Russo, Alejandro, 1978, et al.
(författare)
-
Securing Interaction between Threads and the Scheduler in the Presence of Synchronization
- 2009
-
Ingår i: Journal of Logic and Algebraic Programming. - : Elsevier BV. - 1567-8326. ; 78:7, s. 593-618
-
Tidskriftsartikel (refereegranskat)abstract
- The problem of information flow in multithreaded programs remains an important open challenge. Existing approaches to specifying and enforcing information-flow security often suffer from over-restrictiveness, relying on nonstandardsemantics, lack of compositionality, inability to handle dynamic threads,inability to handle synchronization, scheduler dependence, and efficiency overheadfor the code that results from security-enforcing transformations. This paper suggests a remedy for some of these shortcomings by developing a novel treatment of the interaction between threads and the scheduler. As a result, we present a permissive noninterference-like security specification and a compositional security type system that provably enforces this specification. The type system guarantees security for a wide class of schedulers and provides a flexible and efficiency-friendly treatment of dynamic threads.
|
|
| 10. |
- Solin, Kim
(författare)
-
Normal forms in total correctness for while programs and action systems
- 2011
-
Ingår i: Journal of Logic and Algebraic Programming. - : Elsevier BV. - 1567-8326 .- 1873-5940. ; 80:6, s. 362-375
-
Tidskriftsartikel (refereegranskat)abstract
- A classical while-program normal-form theorem is derived in demonic refinement algebra. In contrast to Kozen's partial-correctness proof of the theorem in Kleene algebra with tests, the derivation in demonic refinement algebra provides a proof that the theorem holds in total correctness. A normal form for action systems is also discussed.
|
|
