| 1. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
A coordination protocol language for power grid operation control
- 2019
-
Ingår i: Journal of Logical and Algebraic Methods in Programming. - : Elsevier BV. - 2352-2208 .- 2352-2216. ; 109
-
Tidskriftsartikel (refereegranskat)abstract
- Future power distribution grids will comprise a large number of components, each potentially able to carry out operations autonomously. Clearly, in order to ensure safe operation of the grid, individual operations must be coordinated among the different components. Since operation safety is a global property, modelling component coordination typically involves reasoning about systems at a global level. In this paper, we propose a language for specifying grid operation control protocols from a global point of view. In our model, operation control is yielded in communications driven by both the grid topology and by state-based information, features captured by novel language principles previously unexplored. We show how the global specifications can be used to automatically generate local controllers of individual components, and that the distributed implementation yielded by such controllers operationally corresponds to the global specification. We showcase our development by modelling a fault management scenario in power grids. (C) 2019 Elsevier Inc. All rights reserved.
|
|
| 2. |
- Abrahamsson, Oskar, 1986
(författare)
-
A verified proof checker for higher-order logic
- 2020
-
Ingår i: Journal of Logical and Algebraic Methods in Programming. - : Elsevier BV. - 2352-2208 .- 2352-2216. ; 112
-
Tidskriftsartikel (refereegranskat)abstract
- We present a computer program for checking proofs in higher-order logic (HOL) that is verified to accept only valid proofs. The proof checker is defined as functions in HOL and synthesized to CakeML code, and uses the Candle theorem prover kernel to check logical inferences. The checker reads proofs in the OpenTheory article format, which means proofs produced by various HOL proof assistants are supported. The proof checker is implemented and verified using the HOL4 theorem prover, and comes with a proof of soundness. (C) 2020 Elsevier Inc. All rights reserved.
|
|
| 3. |
- Alshareef, Hanaa, 1985, et al.
(författare)
-
A collaborative access control framework for online social networks
- 2020
-
Ingår i: Journal of Logical and Algebraic Methods in Programming. - : Elsevier BV. - 2352-2208 .- 2352-2216. ; 114
-
Tidskriftsartikel (refereegranskat)abstract
- Most Online Social Networks allow users to set their privacy settings concerning posting information, but current implementations do not allow a fine grained enforcement in case the posted item concerns other users. In this paper we propose a new collaborative access control framework that takes into account the relation of multiple users for viewing as well as for sharing items, eventually solving conflicts in the privacy settings of the users involved. Our solution relies on two algorithms, one for viewing and another one for sharing items. We provide an evaluation of these algorithms where we demonstrate how varying some of the parameters directly influences the decision of viewing or sharing an item. Last but not least, we present a proof-of-concept implementation of our approach in an open source social network called Diaspora. (C) 2020 Elsevier Inc. All rights reserved.
|
|
| 4. |
|
|
| 5. |
- Beohar, Harsh, 1984-, et al.
(författare)
-
Input–output conformance testing for software product lines
- 2016
-
Ingår i: The Journal of logical and algebraic methods in programming. - Amsterdam : Elsevier. - 2352-2208 .- 2352-2216. ; 85:6, s. 1131-1153
-
Tidskriftsartikel (refereegranskat)abstract
- We extend the theory of input-output conformance (IOCO) testing to accommodate behavioral models of software product lines (SPLs). We present the notions of residual and spinal testing. These notions allow for structuring the test process for SPLs by taking variability into account and extracting separate test suites for common and specific features of an SPL. The introduced notions of residual and spinal test suites allow for focusing on the newly introduced behavior and avoiding unnecessary re-test of the old one. Residual test suites are very conservative in that they require retesting the old behavior that can reach to new behavior. However, spinal test suites more aggressively prune the old tests and only focus on those test sequences that are necessary in reaching the new behavior. We show that residual testing is complete but does not usually lead to much reduction in the test-suite. In contrast, spinal testing is not necessarily complete but does reduce the test-suite. We give sufficient conditions on the implementation to guarantee completeness of spinal testing. Finally, we specify and analyze an example regarding the Ceiling Speed Monitoring Function from the European Train Control System. (C) 2016 The Author(s). Published by Elsevier Inc.
|
|
| 6. |
- Camilleri, John J., 1986, et al.
(författare)
-
Modelling and analysis of normative documents
- 2017
-
Ingår i: Journal of Logical and Algebraic Methods in Programming. - : Elsevier BV. - 2352-2208 .- 2352-2216. ; 91, s. 33-59
-
Tidskriftsartikel (refereegranskat)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.
|
|
| 7. |
- Castegren, Elias, et al.
(författare)
-
Bestow and Atomic : Concurrent programming using isolation, delegation and grouping
- 2018
-
Ingår i: The Journal of logical and algebraic methods in programming. - : Elsevier BV. - 2352-2208 .- 2352-2216. ; 100, s. 130-151
-
Tidskriftsartikel (refereegranskat)abstract
- Any non-trivial concurrent system warrants synchronisation, regardless of the concurrency model. Actor-based concurrency serialises all computations in an actor through asynchronous message passing. In contrast, lock-based concurrency serialises some computations by following a lock-unlock protocol for accessing certain data. Both systems require sound reasoning about pointers and aliasing to exclude data-races. If actor isolation is broken, so is the single-thread-of-control abstraction. Similarly for locks, if a datum is accessible outside of the scope of the lock, the datum is not governed by the lock. In this paper we discuss how to balance aliasing and synchronisation. In previous work, we defined a type system that guarantees data-race freedom of actor-based concurrency and lock-based concurrency. This paper extends this work by the introduction of two programming constructs; one for decoupling isolation and synchronisation and one for constructing higher-level atomicity guarantees from lower-level synchronisation. We focus predominantly on actors, and in particular the Encore programming language, but our ultimate goal is to define our constructs in such a way that they can be used both with locks and actors, given that combinations of both models occur frequently in actual systems. We discuss the design space, provide several formalisations of different semantics and discuss their properties, and connect them to case studies showing how our proposed constructs can be useful. We also report on an on-going implementation of our proposed constructs in Encore.
|
|
| 8. |
|
|
| 9. |
|
|
| 10. |
- Coto, Alex, et al.
(författare)
-
An abstract framework for choreographic testing
- 2021
-
Ingår i: The Journal of logical and algebraic methods in programming. - : Elsevier BV. - 2352-2208 .- 2352-2216. ; 123
-
Tidskriftsartikel (refereegranskat)abstract
- We present a tool-supported approach for the model-driven testing of message-passing applications. Our approach envisages choreographies as a particularly suited model to derive tests in order to tame the problems of correctness of distributed applications.
|
|
