Search

In this paper, we propose an approach to extend the operational time of teams of battery-based robots by introducing a set of charging stations. We assume that the robots are heterogeneous (having different energy limits and being able to service different types of customers) and have access to a priori known map of the environment. The map is modeled as a directed, connected, and finite graph whose nodes are charging stations or customers, and arcs denote the possibility of traveling. To this end, we first formulate a task assignment and path planning problem that aims at optimizing energy consumption as well as the time needed to complete the tasks, including the time spent for recharging. Next, we propose four offline optimization techniques and one online algorithm, where the robots can dynamically adjust their paths in response to the presence of uncertainties imposed by the physical environment. Our proposed algorithms are validated through both simulation and a real-world case study on a team of unmanned aerial vehicles (UAVs) performing a joint search mission.

Aqueous zinc/manganese dioxide batteries are excellent candidates for stationary energy storage applications due to several advantages, including low cost, the earth-abundance of Zn and Mn-oxides, high theoretical volumetric and specific capacity. The hausmannite phase of manganese oxide (Mn 3 O 4 ) has been studied for rechargeable near-neutral (2 M ZnSO 4 ) zinc-manganese oxide battery applications. Electrochemical investigation in coin cell hardware reveals that Mn 3 O 4 activation occurs during the initial ≈ 45 cycles, after which maximum capacity was achieved. More than 65% of its maximum capacity was retained for more than 800 charge/discharge cycles showing excellent reversibility of the material. XRD analysis shows no phase change of Mn 3 O 4 during the cycling. Identification and characterization of new Mn-oxide polymorphs, which lead to improved battery performance, are a critical contribution to the field of energy storage. With further improvements, this battery chemistry and its variations, have the potential to meet the requirements for grid-level storage applications.

In this paper, we consider runtime verification of synchronous distributed systems, where a decentralized set of monitors that only have a partial view of the system are subject to crash failures. In this context, it is unavoidable that monitors may have different views of the underlying system, and, therefore, have different opinions about the correctness property. We propose an automata-based synchronous monitoring algorithm that copes with t crash monitor failures. Moreover, local monitors do not communicate their explicit reading of the underlying system. Rather, they emit a symbolic verdict that efficiently encodes their partial views. This significantly reduces the communication overhead.

Although randomized algorithms have widely been used in distributed computing as a means to tackle impossibility results, it is currently unclear what type of randomization leads to the best performance in such algorithms. This paper proposes three automated techniques to find the probability distribution that achieves minimum average recovery time for an input randomized distributed self-stabilizing protocol without changing the behavior of the algorithm. Our first technique is based on solving symbolic linear algebraic equations in order to identify fastest state reachability in parametric discrete-time Markov chains. The second approach applies parameter synthesis techniques from probabilistic model checking to compute the rational function describing the average recovery time and then uses dedicated solvers to find the optimal parameter valuation. The third approach computes over- and under-approximations of the result for a given parameter region and iteratively refines the regions with minimal recovery time up to the desired precision. The latter approach finds sub-optimal solutions with negligible errors, but it is significantly more scalable in orders of magnitude as compared to the other approaches.

The classic vehicle routing problem (VRP) is generally concerned with the optimal design of routes by a fleet of vehicles to service a set of customers by minimizing the overall cost, usually the travel distance for the whole set of routes. Although the problem has been extensively studied in the context of operations research and optimization, there is little research on solving the VRP, where distributed vehicles need to compute their respective routes in a decentralized fashion. Our first contribution is a synchronous distributed approximation algorithm that solves the VRP. Using the duality theorem of linear programming, we show that the approximation ratio of our algorithm is O(n · (ρ)1/n log(n + m)), where ρ is the maximum cost of travel or service in the input VRP instance, n is the size of the graph, and m is the number of vehicles. We report results of simulations and discuss implementation of our algorithm on a real fleet of unmanned aerial systems (UASs) that carry out a set of tasks.

This paper introduces a novel runtime verification technique for a rich sub-class of Clarkson and Schneider's hyperproperties. The primary application of such properties is in expressing security policies (e.g., information flow) that cannot be expressed in trace-based specification languages (e.g., LTL). First, to incorporate syntactic means, we draw connections between safety and co-safety hyperproperties and the temporal logic HYPERLTL, which allows explicit quantification over multiple executions. We also define the notion of monitorability in HYPERLTL and identify classes of monitorable HYPERLTL formulas. Then, we introduce an algorithm for monitoring k-safety and co-k-safety hyperproperties expressed in HYPERLTL. Our technique is based on runtime formula progression as well as on-the-fly monitor synthesis across multiple executions. We analyze different performance aspects of our technique by conducting thorough experiments on monitoring security policies for information flow and observational determinism on a real-world location-based service dataset as well as synthetic trace sets.

A self-stabilizing system is one that converges to a legitimate state from any arbitrary state. Such an arbitrary state may be reachable due to wrong initialization or the occurrence of transient faults. Average recovery time of self-stabilizing systems is a key factor in evaluating their performance, especially in the domain of network and robotic protocols. This paper introduces a groundbreaking result on automated repair and synthesis of self-stabilizing protocols whose average recovery time is required to satisfy certain constraints. We show that synthesizing and repairing weak-stabilizing protocols under average recovery time constraints is NP-complete. To cope with the exponential complexity (unless P = NP), we propose a polynomial-time heuristic.

Runtime verification is a lightweight automated formal method for specification-based runtime monitoring as well as testing of large real-world systems. While numerous techniques exist for runtime verification of sequential programs, there has been very little work on specification-based monitoring of distributed systems. In this paper, we propose the first sound and complete method for runtime verification of asynchronous distributed programs for the 3-valued semantics of LTL specifications defined over the global state of the program. Our technique for evaluating LTL properties is inspired by distributed computation slicing, an approach for abstracting distributed computations with respect to a given predicate. Our monitoring technique is fully decentralized in that each process in the distributed program under inspection maintains a replica of the monitor automaton. Each monitor may maintain a set of possible verification verdicts based upon existence of concurrent events. Our experiments on runtime monitoring of a simulated swarm of flying drones show that due to the design of our Algorithm, monitoring overhead grows only in the linear order of the number of processes and events that need to be monitored.

Power efficiency has been one of the main objectives of hardware design in the last two decades. However, with the recent explosion of mobile computing and the increasing demand for green data centers, software power efficiency has also risen to be an equally important factor. We argue that most classic concurrency control algorithms were designed in an era when power efficiency was not an important dimension in algorithm design. Such algorithms are applied to solve a wide range of problems from kernel-level primitives in operating systems to networking devices and web services. These primitives and services are constantly and heavily invoked in any computer system and by larger scale in networking devices and data centers. Thus, even a small change in their power spectrum can make a huge impact on overall power consumption in long periods of time. This paper focuses on the classic producer-consumer problem. First, we study the power efficiency of different existing implementations of the producer-consumer problem. In particular, we present evidence that these implementations behave drastically differently with respect to power consumption. Secondly, we present a dynamic algorithm for the multiple producer-consumer problem, where consumers in a multicore system use learning mechanisms to predict the rate of production, and effectively utilize this prediction to attempt to latch onto previously scheduled CPU wake-ups. Such group latching results in minimizing the overall number of CPU wakeups and in effect, power consumption. We enable consumers to dynamically reserve more pre-allocated memory in cases where the production rate is too high. Consumers may compete for the extra space and dynamically release it when it is no longer needed. Our experiments show that our algorithm provides up to 40% decrease in the number of CPU wakeups, and 30% decrease in power consumption. We validate the scalability of our algorithm with an increasing number of consumers.

The goal of runtime verification is to inspect the correctness of a system by incorporating a monitor during its execution. Predictability of time distribution of monitor invocations and memory usage are two indicators of the quality of a monitoring solution, specially in cyber-physical systems, where the physical environment is a part of the system dynamics. In our previous work, we proposed a control-theoretic approach for coordinating time predictability and memory utilization in runtime verification of time-sensitive systems. To this end, we designed controllers that attempt to improve time predictability, while ensuring the soundness of verification by incorporating a maximally utilized bounded memory buffer that accumulates events.Since the frequency of occurrence of environment actions in cyber-physical systems is not known a priori, the system may run into situations, where the buffer is full, but a monitor invocation has not yet been scheduled. In control theory, this is called the overshooting phenomenon, which inherently decreases time predictability. In this paper, we address the issue of overshoots, by employing a second controller that allows limited memory reservations to temporarily extend the size of the event buffer when the system is subject to bursts of environment actions. We apply our solution to the verification of the air/fuel ratio in a car engine exhaust. The acceptable ratio varies depending on the driving circumstances, and monitoring that ratio is important to control emissions in a vehicle. A highly predictable monitor imposes uniform load on the engine control unit (ECU), thus, not negatively or sporadically affecting its control tasks. The experimental results exhibit two significant contributions: we (1) demonstrate the advantages of applying our approach to achieve low variation in the frequency of monitor invocations for verication, while maintaining maximum memory utilization, and (2) clearly illustrate that by negligible temporary increases in the size of the event buffer, the number of overshoots decreases significantly, which in turn substantially increases time predictability of runtime verication.

International audience; We propose a new metric for effectively and accurately evaluating the performance of self-stabilizing algorithms. Self-stabilization is a versatile category of fault-tolerance that guarantees system recovery to normal behavior within a finite number of steps, when the state of the system is perturbed by transient faults (or equally, the initial state of the system can be some arbitrary state). The performance of self-stabilizing algorithms is conventionally characterized in the literature by asymptotic computation complexity. We argue that such characterization of performance is too abstract and does not reflect accurately the realities of deploying a distributed algorithm in practice. Our new metric for characterizing the performance of self-stabilizing algorithms is the expected mean value of recovery time. Our metric has several crucial features. Firstly, it encodes accurate average case speed of recovery. Secondly, we show that our evaluation method can effectively incorporate several other parameters that are of importance in practice and have no place in asymptotic computation complexity. Examples include the type of distributed scheduler, likelihood of occurrence of faults, the impact of faults on speed of recovery, and network topology. We utilize a deep analysis technique, namely, probabilistic model checking to rigorously compute our proposed metric. All our claims are backed by detailed case studies and experiments.

Runtime verification is a monitoring technique to gain assurance about well-being of a program at run time. Most existing approaches use sequential monitors; i.e., when the state of the program with respect to an event of interest changes, the monitor interrupts the program execution, evaluates a set of logical properties, and finally resumes the program execution. In this paper, we propose a GPU-based method for design and implementation of monitors that enjoy two levels of parallelism: the monitor (1) works along with the program in parallel, and (2) evaluates a set of properties in a parallel fashion as well. Our parallel monitoring algorithms effectively exploit the many-core platform available in the GPU. In addition to parallel processing, our approach benefits from a true separation of monitoring and functional concerns, as it isolates the monitor in the GPU. Our method is fully implemented and experimental results show significant reduction in monitoring overhead, monitoring interference, and power consumption due to leveraging the GPU technology.

Runtime monitoring aims at analyzing the well-being of a system at run time in order to detect errors and steer the system towards a healthy behavior. Such monitoring is a complementary technique to other approaches for ensuring correctness, such as formal verification and testing. In time-triggered runtime monitoring, a monitor runs as a separate process in parallel with an application program under scrutiny and samples the program's state periodically to evaluate a set of properties. Applying this technique in a computing system results in obtaining bounded and predictable overhead. Gaining such characteristics for overhead is highly desirable for designing and engineering time-critical applications, such as safety-critical embedded systems. However, a time-triggered monitor requires certain synchronization features at operating system level and may suffer from various concurrency and synchronization dependencies and overheads as well as possible unreliability of synchronization primitives in a real-time setting. In this paper, we propose a new method, where the program under inspection is instrumented, so that it self-samples its state in a periodic fashion without requiring assistance from an external monitor or internal timer. We call this technique time-triggered self-monitoring. First, we formulate an optimization problem for minimizing the number of points in a program, where self-sampling instrumentation instructions must be inserted. We show that this problem is NP-complete. Consequently, we propose a SAT-based solution and a heuristic to cope with the exponential complexity. Our experimental results show that a time-triggered self-monitored program performs significantly better than the same program monitored by an external time-triggered monitor.

Recently, by increasing the usage of battery-powered systems such as laptop, mobile, wristwatch and etc. power dissipation is becoming an important constraint in each electronically design. To reduce the power dissipation, it has been offered to use a floating gate MOSFET technology. According to decline the size of the circuits and power dissipation, thickness of the gate oxide will decrease and this causes a big leakage current in the VLSI circuits. So, new methods should be recommended to maintain the charges in the nodes. In this paper we try to present a new Quasi FGMOS technique to solve this problem. Simulations in a 65 nm process show that by using our proposed Quasi FGMOS, there will be lower PDP and also leakage current than conventional Quasi FGMOSs have.

Automated formal analysis methods such as program verification and synthesis algorithms often suffer from time complexity of their decision procedures and also high space complexity known as the state explosion problem. Symbolic techniques, in which elements of a problem are represented by Boolean formulae, are desirable in the sense that they often remedy the state explosion problem and time complexity of decision procedures. Although symbolic techniques have successfully been used in program verification, their benefits have not yet been exploited in the context of program synthesis and transformation extensively. In this paper, we present a symbolic method for automatic synthesis of fault-tolerant distributed programs. Our experimental results on synthesis of classical fault-tolerant distributed problems such as Byzantine agreement and token ring show a significant performance improvement by several orders of magnitude in both time and space complexity. To the best of our knowledge, this is the first illustration where programs with large state space (beyond 2100) is handled during synthesis.

We study the runtime verification of hyperproperties, expressed in the temporal logic HyperLTL, as a means to inspect a system with respect to security polices. Runtime monitors for hyperproperties analyze trace logs that are organized by common prefixes in the form of a tree-shaped Kripke structure, or are organized both by common prefixes and by common suffixes in the form of an acyclic Kripke structure. Unlike runtime verification techniques for trace properties, where the monitor tracks the state of the specification but usually does not need to store traces, a monitor for hyperproperties repeatedly model checks the growing Kripke structure. This calls for a rigorous complexity analysis of the model checking problem over tree-shaped and acyclic Kripke structures. We show that for trees, the complexity in the size of the Kripke structure is L-complete independently of the number of quantifier alternations in the HyperLTL formula. For acyclic Kripke structures, the complexity is PSPACE-complete (in the level of the polynomial hierarchy that corresponds to the number of quantifier alternations). The combined complexity in the size of the Kripke structure and the length of the HyperLTL formula is PSPACE-complete for both trees and acyclic Kripke structures, and is as low as NC for the relevant case of trees and alternation-free HyperLTL formulas. Thus, the size and shape of both the Kripke structure and the formula have significant impact on the complexity of the model checking problem.