1,721,066 research outputs found
Accuracy of message counting abstraction in fault-tolerant distributed algorithms
Get PDFFault-tolerant distributed algorithms are a vital part of mission-critical distributed systems. In principle, automatic verification can be used to ensure the absence of bugs in such algorithms. In practice however, model checking tools will only establish the correctness of distributed algorithms if message passing is encoded efficiently. In this paper, we consider abstractions suitable for many fault-tolerant distributed algorithms that count messages for comparison against thresholds, e.g., the size of a majority of processes. Our experience shows that storing only the numbers of sent and received messages in the global state is more efficient than explicitly modeling message buffers or sets of messages. Storing only the numbers is called message-counting abstraction. Intuitively, this abstraction should maintain all necessary information. In this paper, we confirm this intuition for asynchronous systems by showing that the abstract system is bisimilar to the concrete system. Surprisingly, if there are real-time constraints on message delivery (as assumed in fault-tolerant clock synchronization algorithms), then there exist neither timed bisimulation, nor time-abstracting bisimulation. Still, we prove this abstraction useful for model checking: it preserves ATCTL properties, as the abstract and the concrete models simulate each other
Going Beyond Counting First Authors in Author Co-citation Analysis
Get PDFThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
Variations on the Author
Get PDF“Variations on the Author” discusses two of Eduardo Coutinho’s recent films (Um Dia na Vida, from 2010, and Últimas Conversas, posthumously released in 2015) and their contribution to the general question of documentary authorship. The director’s filmography is characterized by a consistent yet self-effacing form of authorial self-inscription: Coutinho often features as an interviewer that rather than express opinions propels discourses; an interviewer that is good at listening. This mode of self-inscription characterizes him as an author who is not expressive but who is nonetheless markedly present on the screen. In Um Dia na Vida, however, Coutinho is completely absent form the image, while Últimas Conversas, on the contrary, includes a confessional prologue that moves the director from the margins to the center of his films. This article examines the ways in which these works stand out in the filmography of a director who offers new insights into the notion of cinematic authorship
Reduction techniques for parameterized model checking and synthesis of fault-tolerant distributed algorithms
Get PDFDistributed algorithms have many applications in everyday life, as well as in avionic and automotive embedded systems, computer networks, and the Internet of Things. The central idea is to achieve dependability by replication, and to ensure that all correct replicas behave as one, even if some of the replicas fail. In this way, the correct operation of the system is more reliable than the correct operation of its parts. Fault-tolerant algorithms are typically used in applications where highest reliability is required because human lives might be at risk, such as in automotive or avionic industries, and even unlikely failures of the system are not acceptable. Therefore, correctness of fault-tolerant algorithms is of utmost importance. New application domains, such as cloud computing or blockchain technologies, provide new motivation to study fault-tolerant algorithms. With the huge number of computers involved, faults are the norm rather than the exception. Consequently, fault-tolerance becomes an economic necessity, and so does the correctness of mechanisms for fault-tolerance. In order to deal with real-life distributed systems with thousands of components, we need techniques for analyzing fault-tolerant distributed algorithms for every system size, that is, for every number of components and every admissible number of faults. We use special variables n, f and t, called parameters, to describe the number of processes in the system, the number of faults, and an upper bound on the number of faults, respectively. An algorithm is considered to be correct if it satisfies its specifications for every n; f; t, under a certain prerequisite, e.g., n > 3t, called resilience condition. Verifying such general correctness is called parameterized verification, and synthesizing correct algorithms from their specifications is in this case called parameterized synthesis. Reasoning about correctness of fault-tolerant distributed algorithms (FTDAs) is an immensely difficult task, due to the non-deterministic behavior caused by the presence of faults, concurrency, message delays, etc. The classical approach toward correctness consists of pencil-and-paper mathematical proofs, that require human ingenuity and huge manual eorts. As distributed algorithms show complex behavior, and are difficult to understand for human engineers, there is only very limited tool support to catch logical errors in fault-tolerant distributed algorithms, especially at design time. In this thesis we focus on the class of asynchronous FTDAs where processes communicate by message passing and compare numbers of received messages against so-called thresholds. For instance, a process might be allowed to perform an action only if it has received messages from a majority of processes in the system, i.e., at least n 2 messages. Thresholds are typically linear combinations of parameters, and thus they constitute a parameterization of the code itself. For asynchronous FTDAs, most existing verification and synthesis techniques are either only able to deal with small instances, for example, with four processes among which one might fail, or they cannot deal with (i) parameterized code, (ii) arithmetic resilience conditions, or (iii) specifications of distributed algorithms. In this thesis we develop techniques for the parameterized analysis of this class of FTDAs that can cope with all the mentioned challenges. More specifically, our methods are based on reduction techniques, that is, on reasoning about dependency of concurrently executed events. The contribution of this thesis is threefold: (1) We present a complete framework for the parameterized verification of temporal properties of this particular class of FTDAs, that is, a method for certifying the correctness of an algorithm for any system size. Our method addresses both safety and liveness speci cations of algorithms. (2) We introduce an automated technique for synthesizing FTDAs that are correct for any system size, rather than for a fixed size. In fact, for a given so-called skeleton of an algorithm from our class, we automatically detect thresholds, parameterized in the number of processes in total and the number of faults, that yield correct algorithms. (3) Additionally, we extend the class of the considered algorithms, by allowing probabilistic transitions, such as coin tosses, and specifications that hold with probability 1. We reduce the problem of veri cation of such randomized FTDAs to the non-probabilistic setting. In this way, we present the first automated method for parameterized verification of randomized fault-tolerant distributed algorithms and their associated probabilistic properties
Appropriate Similarity Measures for Author Cocitation Analysis
Get PDFWe provide a number of new insights into the methodological discussion about author cocitation analysis. We first argue that the use of the Pearson correlation for measuring the similarity between authors’ cocitation profiles is not very satisfactory. We then discuss what kind of similarity measures may be used as an alternative to the Pearson correlation. We consider three similarity measures in particular. One is the well-known cosine. The other two similarity measures have not been used before in the bibliometric literature. Finally, we show by means of an example that our findings have a high practical relevance.information science;Pearson correlation;cosine;similarity measure;author cocitation analysis
SMT-driven techniques for verifying distributed systems
Get PDFDistributed systems, that is, networks of real or virtual components that collaborate in solving an algorithmic task underpin many of our modern technologies. The correctness of these systems is often critical; unpredictable system behavior can, in the worst cases, result in major financial loss, confidential data breaches, or even physical harm. Because of this, formal verification of these systems has been an active area of research for many decades. With the advent of cloud services and cryptocurrencies, there has also been an increase in demand, for newer, better, and more robust verification techniques. The primary contribution of this thesis is a set of techniques for designing a symbolic model checker for TLA+, with which one can verify properties of distributed algorithms. We focus particularly on specifications of distributed algorithms, as the use of TLA+ has recently been seeing rapid growth in the development of distributed systems. Specifically, we: 1. Formalize the notion of a symbolic transition, an equivalence class of transitions in the state-space defined by an algorithm specification. This is both a necessary prerequisite for symbolic verification, as well as a finite abstraction, reducing a potentially infinite number of real transitions, to a finite family of symbolic ones. 2. Define an encoding of constructs in the kernel of TLA+ to first-order logic, suitable for SMT solvers. This allows us to symbolically encode a bounded execution of the algorithm specification, and the properties we wish to verify, as an SMT formula, which can be passed to an off-the-shelf SMT solver. 3. Design a type system for TLA+, as well as a technique for automatic type inference. Types are both necessary, to bridge the gap between conventionally untyped TLA+ and typed SMT, and helpful, because algorithm designers are typically familiar with types and their uses in programming languages, and many errors, especially in the incremental design of an algorithm, can already be caught by type analysis
Dispelling the Myths Behind First-author Citation Counts
Get PDFWe conducted a full-scale evaluative citation analysis study of scholars in the XML research field to explore just how different from each other author rankings resulting from different citation counting methods actually are, and to demonstrate the capability of emerging data and tools on the Web in supporting more realistic citation counting methods. Our results contest some common arguments for the continued
use of first-author citation counts in the evaluation of scholars, such as high correlations between author rankings by first-author citation counts and other citation
counting methods, and high costs of using more realistic citation counting methods that are not well-supported by the ISI databases. It is argued that increasingly available digital full text research papers make it possible for citation analysis studies to go beyond what the ISI databases have directly supported and to employ more
sophisticated methods
Symbolic verification of TLA+ specifications with applications to distributed algorithms
Get PDFTLA+ is a language for formal specification of concurrent and distributed protocols. TLA+ is extremely concise yet expressive: The language primitives include Booleans, integers, functions, tuples, records, sequences, and sets thereof, which can be also nested. This is probably why the only model checker for TLA+ (called TLC) relies on explicit enumeration of values and states. This thesis has two main parts. First, we bring symbolic verification to the specification language TLA+. Second, we focus on formal verification techniques for the partial synchrony model of distributed computations. We demonstrate our methodology and approaches to the second part by conducting a case study about the Chandra and Toueg failure detector. Part 1. In this thesis, we first bring symbolic verification to TLA+ specifications by developing the symbolic model checker called APALACHE. Like TLC, APALACHE assumes that all specification parameters are fixed and all states are finite structures. Unlike TLC, APALACHE translates the underlying transition relation into quantifier-free SMT constraints, which allows us to exploit the power of SMT solvers. Designing this translation is the central challenge that we address in the first part of this thesis. Our experiments show that APALACHE outperforms TLC on checking inductive invariants and finding counterexamples in instances with large state spaces. In TLA+, a specification is written as a logical formula without assignments and other imperative statements. To improve APALACHE's performance, we introduce an automatic technique to slice a TLA+ specification in symbolic transitions, which are used as an input to APALACHE. In contrast to TLC, our technique does not explicitly evaluate expressions, but it reduces the problem of finding symbolic transitions to the satisfiability of an SMT formula. Part 2. In the second part of this thesis, we focus on symbolic verification techniques for partial synchrony that is a model of computation in distributed algorithms and modern blockchains. In this model, correctness of algorithms requires the existence of bounds ∆ on message delays and φ on the relative speed of processes after reaching Global Stabilization Time (GST). This makes partially synchronous algorithms parametricin time bounds. Moreover, partially synchronous algorithms are parameterized in the number of processes. Therefore, in general we cannot verify all instances of a partially synchronous distributed algorithm by applying APALACHE or other state-of-the-art model checkers, e.g., TLC, Spin, or NuSMV.The failure detector of Chandra and Toueg is a well-known algorithm to detect crashed processes in a system. Importantly, correctness of the failure detector is based only on the existence of bounds ∆ and φ after GST. Hence, we choose the failure detector as a case study in our thesis. To verify all instances of the failure detector, we develop the two following techniques.While the general parameterized verification is undecidable, many distributed algorithms such as mutual exclusion, cache coherence, and distributed consensus enjoy the cutoff property, which reduces the parameterized verification problem to verification of a finite number of instances. The failure detector does not fall into one of the known classes since they typically rely on point-to-point communication and timeouts. In this thesis, we formalize this communication structure and introduce the class of symmetric point-to-point algorithms. We show that the symmetric point-to-point algorithms have a cutoff. By these results, it is sufficient to verify the failure detector by checking instances with only two processes. We do parametric verification of both safety and liveness of the failure detector in three frameworks: TLA+, counter automata, and IVy. We introduce encoding techniques and an abstraction of in-transit messages to efficiently specify the failure detector in each framework. By running the model checkers for TLA+ (TLC and APALACHE) and counter automata (FAST), we prove safety for fixed time bounds. This helps us to find the inductive invariants for fixed parameters, which we used as a starting point for the proofs with IVy. By running IVy, we prove safety for arbitrary time bounds. Moreover, we show how to verify liveness of the failure detector by reducing the verification problem to safety verification. Thus, both properties are verified by developing inductive invariants with IVy. We conjecture that correctness of other partially synchronous algorithms may be proven by following the presented methodology
- …
