| 1. |
- Dinges, Peter, et al.
(author)
-
Dynamic Probabilistic Inference of Atomic Sets
-
Other publication (other academic/artistic)abstract
- Concurrent programs often ensure the consistency of their data structures through synchronization. Because control-centric synchronization primitives, such as locks, are disconnected from the consistency invariants of the data structures, a compiler cannot check and and enforce these invariants - making it hard to detect bugs caused by incorrect synchronization. Moreover, a consistency bug may be the result of some unlikely schedule and therefore not show up in program testing. In contrast, data-centric synchronization adds annotations to data structures, defining sets of fields that must be accessed atomically. A compiler can check such annotations for consistency, detect deadlock, and automatically add primitives to prevent data races. However, annotating existing code is time consuming and error prone because it requires understanding the concurrency semantics implemented in the code. We propose a novel algorithm, called BAIT, for deriving such annotations automatically from observed program executions using Bayesian probabilistic inference. The algorithm produces atomic set, unit of work, and alias annotations for atomic-set based synchronization. Using our implementation of the algorithm, we have derived annotations for large code bases, for example the Java collections framework, in a matter of seconds. A comparison of the inferred annotations against manually converted programs, and two case studies on large, widely-used programs, show that our implementation derives detailed annotations of high quality.
|
|
| 2. |
- Khamespanah, Ehsan, et al.
(author)
-
Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking
- 2018
-
In: International Journal on Software Tools for Technology Transfer. - : SPRINGER HEIDELBERG. - 1433-2779 .- 1433-2787. ; 20:5, s. 547-561
-
Journal article (peer-reviewed)abstract
- Programmers often use informal worst-case analysis and debugging to ensure that schedulers satisfy real-time requirements. Not only can this process be tedious and error-prone, it is inherently conservative and thus likely to lead to an inefficient use of resources. We propose to use model checking to find a schedule which optimizes the use of resources while satisfying real-time requirements. Specifically, we represent a Wireless sensor and actuator network (WSAN) as a collection of actors whose behaviors are specified using a Java-based actor language extended with operators for real-time scheduling and delay representation. We show how the abstraction mechanism and the compositionality of actors in the actor model may be used to incrementally build a model of a WSAN's behavior from node-level and network models. We demonstrate the approach with a case study of a distributed real-time data acquisition system for high-frequency sensing using Timed Rebeca modeling language and the Afra model checking tool.
|
|
| 3. |
- Khamespanah, Ehsan, et al.
(author)
-
Schedulability Analysis of Distributed Real-Time Sensor Network Applications Using Actor-Based Model Checking
- 2016
-
In: Model Checking Software - 23rd International Symposium SPIN 2016. - Cham : Springer International Publishing. - 9783319325811 ; , s. 165-181
-
Conference paper (peer-reviewed)abstract
- Programmers often use informal worst-case analysis and debugging to ensure schedules that satisfy real-time requirements. Not only can this process be tedious and error-prone, it is inherently conservative and thus likely to lead to an inefficient use of resources. We propose to use model checking to find a schedule which optimizes the use of resources while satisfying real-time requirements. Specifically, we represent a Wireless sensor and actuator network (WSAN) as a collection of actors whose behavior is specified using a C-based actor language extended with operators for real-time scheduling and delay representation. We show how the abstraction and compositionality properties of the actor model may be used to incrementally build a model of a WSAN’s behavior from node-level and network models. We demonstrate the approach with a case study of a distributed real-time data acquisition system for high frequency sensing using Timed Rebeca modeling language and the Afra model checking tool.
|
|
| 4. |
- Lundblad, Andreas, 1983-
(author)
-
Inlined Reference Monitors : Certification,Concurrency and Tree Based Monitoring
- 2013
-
Doctoral thesis (other academic/artistic)abstract
- Reference monitor inlining is a technique for enforcing security policies by injecting security checks into the untrusted software in a style similar to aspect-oriented programming. The intention is that the injected code enforces compliance with the policy (security), without adding behavior (conservativity) or affecting existing policy compliant behavior (transparency).This thesis consists of four papers which covers a range of topics including formalization of monitor inlining correctness properties, certification of inlined monitors, limitations in multithreaded settings and extensions using data-flow monitoring.The first paper addresses the problem of having a potentially complex program rewriter as part of the trusted computing base. By means of proof-carrying code we show how the inliner can be replaced by a relatively simple proof-checker. This technique also enables the use of monitor inlining for quality assurance at development time, while minimizing the need for post-shipping code rewrites.The second paper focuses on the issues associated with monitor inlining in a concurrent setting. Specifically, it discusses the problem of maintaining transparency when introducing locks for synchronizing monitor state reads and updates. Due to Java's relaxed memory model, it turns out to be impossible for a monitor to be entirely transparent without sacrificing the security property. To accommodate for this, the paper proposes a set of new correctness properties shown to be realistic and realizable.The third paper also focuses on problems due to concurrency and identifies a class of race-free policies that precisely characterizes the set of inlineable policies. This is done by showing that inlining of a policy outside this class is either not secure or not transparent, and by exhibiting a concrete algorithm for inlining of policies inside the class which is secure, conservative, and transparent. The paper also discusses how certification in the style of proof-carrying code could be supported in multithreaded Java programs.The fourth paper formalizes a new type of data centric runtime monitoring which combines monitor inlining with taint tracking. As opposed to ordinary techniques which focus on monitoring linear flows of events, the approach presented here relies on tree shaped traces. The paper describes how the approach can be efficiently implemented and presents a denotational semantics for a simple ``while'' language illustrating how the theoretical foundations is to be used in a practical setting.Each paper is concluded by a practical evaluation of the theoretical results, based on a prototype implementation and case studies on real-world applications and policies.
|
|
| 5. |
- Sirjani, Marjan, et al.
(author)
-
A compositional approach for modeling and timing analysis of wireless sensor and actuator networks
- 2017
-
In: ACM SIGBED Review. - : Association for Computing Machinery (ACM). - 1551-3688. ; 14:3, s. 49-56
-
Journal article (peer-reviewed)abstract
- Wireless sensor and actuator networks (WSAN) are created through the integration of multiple nodes which acquire data and perform reaction based on them. In a general overview, sensor nodes of WSANs are responsible for data acquisition and sending them to a central node. The central node stores all the received data and performs reactions. Timing verification of WSAN applications to ensure schedulability of tasks is a challenge, and is generally performed by worst-case analysis. This process is error-prone and inherently conservative. On the other hand, using model checking for analyzing WSAN applications results in state space explosion even for middle-sized configurations. The reason is the necessity of considering the interleaving of the large number of sensors in WSANs. In this paper, we show how to build an actor-based model of WSAN applications, starting from sensor node-level and moving towards the full system, and we show how this compositional modeling improves analysability and modifiability. Realtime extension of actor model is appropriate for modeling WSAN applications where we have many concurrent and asynchronous processes, and interdependent realtime deadlines. We demonstrate the approach using a case study of a distributed realtime data acquisition system for high-frequency sensing, where Timed Rebeca is used for modeling. We use model checking to check the intra/inter-sensor node schedulability.
|
|
