We introduce an automated parameterized verification method for fault-tolerant distributed algorithms (FTDA). FTDAs are parameterized by both the number of processes and the assumed maximum number of faults. At the ce...
详细信息
ISBN:
(纸本)9780983567837
We introduce an automated parameterized verification method for fault-tolerant distributed algorithms (FTDA). FTDAs are parameterized by both the number of processes and the assumed maximum number of faults. At the center of our technique is a parametric interval abstraction (PIA) where the interval boundaries are arithmetic expressions over parameters. Using PIA for both data abstraction and a new form of counter abstraction, we reduce the parameterized problem to finite-state model checking. We demonstrate the practical feasibility of our method by verifying safety and liveness of several fault-tolerant broadcasting algorithms, and finding counter examples in the case where there are more faults than the FTDA was designed for.
This paper considers the PageRank centrality computation problem on large graphs. We study asynchronous and distributed algorithms which are operated by aggregating information from local neighbors iteratively. Unlike...
详细信息
ISBN:
(纸本)9781728176055
This paper considers the PageRank centrality computation problem on large graphs. We study asynchronous and distributed algorithms which are operated by aggregating information from local neighbors iteratively. Unlike prior works which rely on stochastic gradient descent (SGD) applied on a least square objective, we derive a stochastic approximation (SA) scheme for solving the PageRank problem by discretizing a linear system of ordinary differential equations. Our approach results in a family of asynchronous and distributed algorithms applicable for fixed and random topologies. Convergence rates are analyzed for both settings. In the fixed topology setting, we prove that the SA-based PageRank algorithm converges faster than the prior SGD-based method for large graphs. Numerical experiments support our findings.
Transmission power control is one of the key enabling technologies in opportunistic spectrum sharing for secondary users to optimize their performance without incurring undesirable interference on primary users. Vario...
详细信息
ISBN:
(纸本)9781467325691
Transmission power control is one of the key enabling technologies in opportunistic spectrum sharing for secondary users to optimize their performance without incurring undesirable interference on primary users. Various optimization models and algorithms for different scenarios and design objectives have hence been proposed in related work. While ideally these algorithms can find optimal solutions for power control, in practice it is very likely that the output powers are suboptimal or even infeasible if these algorithms are applied in a distributed environment. The reasons are due to various practical considerations such as the overheads of power training, use of the control channel, and dynamics of primary user activity. To address the problem of unfit outputs thus obtained, we investigate in this paper low-complexity algorithms that can be used in tandem with these distributed algorithms by quickly adapting undesirable solutions for use by secondary users such that feasibility is restored and/or optimality is improved. Compared with the approach of finding a new solution based on linear approximation of the optimization problem, we show through evaluations that the proposed algorithm is simple yet effective in achieving the desired goal.
The verification of distributed algorithms is a challenge for formal techniques supported by tools, as model checkers and proof assistants. The difficulties, even for powerful tools, lie in the derivation of proofs of...
详细信息
ISBN:
(纸本)9783030325053;9783030325046
The verification of distributed algorithms is a challenge for formal techniques supported by tools, as model checkers and proof assistants. The difficulties, even for powerful tools, lie in the derivation of proofs of required properties, such as safety and eventuality, for distributed algorithms. Verification by construction can be achieved by using a formal framework in which models are constructed at different levels of abstraction;each level of abstraction is refined by the one below, and this refinement relationships is documented by an abstraction relation namely a gluing invariant. The highest levels of abstraction are used to express the required behavior in terms of the problem domain and the lowest level of abstraction corresponds to an implementation from which an efficient implementation can be derived automatically. In this paper, we describe a methodology based on the general concept of refinement and used for developing distributed algorithms satisfying a given list of safety and liveness properties. The modelling methodology is defined in the Event-B modelling language using the IDE Rodin.
The design and the proof of distributed algorithms are difficult tasks due to the lack of knowledge of the global state and the non determinism in the execution of the processes. Formal methods can guarantee that thes...
详细信息
ISBN:
(纸本)9780769550022
The design and the proof of distributed algorithms are difficult tasks due to the lack of knowledge of the global state and the non determinism in the execution of the processes. Formal methods can guarantee that these algorithms run as designed. In this paper, we show that the proof of complex distributed algorithms can be simplified by combining already proved sub-algorithms. To do so, we use a high level encoding of distributed algorithms in form of graph relabeling systems and we propose a formal proof methodology. The proposed methodology combines refinement and decomposition techniques and relies on the correct-by-construction paradigm used by the Event-B method.
作者：
An, XinPang, JunShandong Univ
Sch Comp Sci & Technol Jinan 250101 Shandong Peoples R China Univ Luxembourg
Comp Sci & Commun 6 Rue Richard Coudenhove Kalergi L-1359 Luxembourg Luxembourg
In the field of distributed computing, there are many round-based algorithms to solve fundamental problems, such as leader election and distributed consensus. Due to the nature of these algorithms, round numbers are u...
详细信息
ISBN:
(纸本)9780769540153
In the field of distributed computing, there are many round-based algorithms to solve fundamental problems, such as leader election and distributed consensus. Due to the nature of these algorithms, round numbers are unbounded and can increase infinitely during executions of the algorithms. This can lead to the state space explosion problem when verifying correctness of these algorithms using model checking. In this paper, we present a general idea of investigating the bounded distance of round numbers in round-based algorithms. We can manage to transform their state spaces into finite by maintaining such relations in a proper way, and thus make automatic verification of these algorithms possible. We apply this idea to several algorithms and present their verification results in the model checker Spin.
An introductory course on distributed systems typically exposes students to some basic synchronization distributed algorithms. This is often the first exposure for these students to the topic of distributed algorithms...
详细信息
ISBN:
(纸本)9781728184784
An introductory course on distributed systems typically exposes students to some basic synchronization distributed algorithms. This is often the first exposure for these students to the topic of distributed algorithms. In addition, in a systems course, these algorithms are typically covered in an informal way, avoiding proofs of correctness or complexity analysis. Hence, this first exposure can be challenging to students. Visualization of these algorithms can help alleviate some of these challenges. We present a suite to visualize six basic algorithms on total ordering, critical sections, and leader election.
distributed systems are inherently complex as they need to address the interplay between features like communication, concurrency, and failure. Due to the inherent complexity of these interacting features, it is typic...
详细信息
ISBN:
(纸本)9781450380492
distributed systems are inherently complex as they need to address the interplay between features like communication, concurrency, and failure. Due to the inherent complexity of these interacting features, it is typically not possible to systematically test these kind of systems;yet, unexpected and unlikely combinations of events might cause corner cases that are hard to find. But since these systems are running typically for long durations, these events are likely to materialize eventually and must be handled correctly. Caught in such a dilemma, students are able to experience the benefits of applying verification tools to check their own algorithms and implementations. Having executable models with automatically generated executions allows them to experiment with different solutions by iteratively adapting and refining their algorithms. In this experience report, we report on our experience of teaching verification in a ( hands-on) distributed systems course. We argue that broadcast algorithms provide a sweet spot in design and verification complexity. To this end, we give an implementation of these algorithms in Erlang and derive a TLA+ specification. TLA+ is a formal language for describing and reasoning about distributed and concurrent systems and provides a model checker, TLC, among other things. Our study reveals interesting parallels between the Erlang and TLA+ code, while exposing the challenges of formally modeling communication and parallelism in distributed systems. Presenting selected aspects of our course design, we aim to motivate the feasibility and need for introducing verification in close correspondence to programming tasks.
We describe a simple algorithm for spectral graph sparsification, based on iterative computations of weighted spanners and uniform sampling. Leveraging the algorithms of Baswana and Sen for computing spanners, we obta...
详细信息
ISBN:
(纸本)9781450328210
We describe a simple algorithm for spectral graph sparsification, based on iterative computations of weighted spanners and uniform sampling. Leveraging the algorithms of Baswana and Sen for computing spanners, we obtain the first distributed spectral sparsification algorithm. We also obtain a parallel algorithm with improved work and time guarantees. Combining this algorithm with the parallel framework of Peng and Spielman for solving symmetric diagonally dominant linear systems, we get a parallel solver which is much closer to being practical and significantly more efficient in terms of the total work.
The coverage problem is of great interest for many sensor network applications, for example, detection of intruders in the sensor field. Topological changes in sensor networks may affect qualities of sensor coverage. ...
详细信息
ISBN:
(纸本)9781595936165
The coverage problem is of great interest for many sensor network applications, for example, detection of intruders in the sensor field. Topological changes in sensor networks may affect qualities of sensor coverage. We present three suites of algorithms for dynamically maintaining the coverage and the measures of its qualities. Using only local knowledge, our algorithms capture the dynamic changes of network topology and efficiently maintain the coverage by updating the radii of sensors combined with limited sensor mobility. Our algorithms have the advantages of low communication complexity with no need of a tight bound on message propagation delay.
暂无评论