An official website of the United States government
Verification is often regarded as a one-time procedure undertaken after a protocol is specified but before it is implemented. However, in practice, protocols continually evolve with the addition of new capabilities and performance optimizations. Existing verification tools are ill-suited to “tracking” protocol evolution and programmers are too busy (or too lazy?) to simultaneously co-evolve specifications manually. This means that the correctness guarantees determined at verification time can erode as protocols evolve. Existing software quality techniques such as regression testing and root cause analysis, which naturally support system evolution, are poorly suited to reasoning about fault tolerance properties of a distributed system because these properties require a search of the execution schedule rather than merely replaying inputs. This paper advocates that our community should explore the intersection of testing and verification to better ensure quality for distributed software and presents our experience evolving a data replication protocol at Elastic using a novel bug-finding technology called Lineage Driven Fault Injection (LDFI) as evidence.
more »
« less
This content will become publicly available on April 28, 2026
Runtime Protocol Refinement Checking for Distributed Protocol Implementations
- Award ID(s):
- 2145471
- PAR ID:
- 10569892
- Publisher / Repository:
- USENIX
- Date Published:
- Subject(s) / Keyword(s):
- Refinement checking Distributed Systems Runtime Verification
- Format(s):
- Medium: X
- Location:
- 22nd USENIX Symposium on Networked Systems Design and Implementation
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
A protocol specifies interactions between roles, which together constitute a multiagent system (MAS). Enacting a protocol presupposes that agents are bound to the its roles. Existing protocol-based approaches, however, do not adequately treat the practical aspects of how roles bindings come about. Pippi addresses this problem of MAS instantiation. It proposes the notion of a metaprotocol, enacting which instantiates a MAS suitable for enacting a given protocol. Pippi demonstrates the subtleties involved in instantiating MAS arising from protocol composition, correlation, and decentralization. To address these subtleties and further support practical application patterns, we introduce an enhanced protocol language, with support for parameter types (including role and protocol typed parameters, for metaprotocols),interface flexibility, and binding constraints. We discuss the realization of our approach through an extended agent architecture,including the novel concept of a MAS adapter for contact management. We evaluate Pippi’s expressiveness by demonstrating common patterns for agent discovery.more » « less
-
Abstract Cetyltrimethylammonium bromide (CTAB)–based methods are widely used to isolate DNA from plant tissues, but the unique chemical composition of secondary metabolites among plant species has necessitated optimization. Research articles often cite a “modified” CTAB protocol without explicitly stating how the protocol had been altered, creating non‐reproducible studies. Furthermore, the various modifications that have been applied to the CTAB protocol have not been rigorously reviewed and doing so could reveal optimization strategies across study systems. We surveyed the literature for modified CTAB protocols used for the isolation of plant DNA. We found that every stage of the CTAB protocol has been modified, and we summarized those modifications to provide recommendations for extraction optimization. Future genomic studies will rely on optimized CTAB protocols. Our review of the modifications that have been used, as well as the protocols we provide here, could better standardize DNA extractions, allowing for repeatable and transparent studies.more » « less
