Multi-Grained Specifications for Distributed System Model Checking and Verification

• URL: http://arxiv.org/abs/2409.14301v3
• Date: Fri, 27 Sep 2024 08:15:53 GMT
• Title: Multi-Grained Specifications for Distributed System Model Checking and Verification
• Authors: Lingzhi Ouyang, Xudong Sun, Ruize Tang, Yu Huang, Madhav Jivrajani, Xiaoxing Ma, Tianyin Xu,
• Abstract summary: We use TLA+ to model fine-grained behaviors of ZooKeeper and the TLC model checker to verify its correctness properties. We show that writing multi-grained specifications is a viable practice and can cope with model-code gaps without untenable state space.
• Score: 9.14614889088682
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper presents our experience specifying and verifying the correctness of ZooKeeper, a complex and evolving distributed coordination system. We use TLA+ to model fine-grained behaviors of ZooKeeper and use the TLC model checker to verify its correctness properties; we also check conformance between the model and code. The fundamental challenge is to balance the granularity of specifications and the scalability of model checking -- fine-grained specifications lead to state-space explosion, while coarse-grained specifications introduce model-code gaps. To address this challenge, we write specifications with different granularities for composable modules, and compose them into mixed-grained specifications based on specific scenarios. For example, to verify code changes, we compose fine-grained specifications of changed modules and coarse-grained specifications that abstract away details of unchanged code with preserved interactions. We show that writing multi-grained specifications is a viable practice and can cope with model-code gaps without untenable state space, especially for evolving software where changes are typically local and incremental. We detected six severe bugs that violate five types of invariants and verified their code fixes; the fixes have been merged to ZooKeeper. We also improve the protocol design to make it easy to implement correctly.

Related papers

• Multi-Convformer: Extending Conformer with Multiple Convolution Kernels [64.4442240213399]
  We introduce Multi-Convformer that uses multiple convolution kernels within the convolution module of the Conformer in conjunction with gating. Our model rivals existing Conformer variants such as CgMLP and E-Branchformer in performance, while being more parameter efficient. We empirically compare our approach with Conformer and its variants across four different datasets and three different modelling paradigms and show up to 8% relative word error rate(WER) improvements.
  arXiv  Detail & Related papers  (2024-07-04T08:08:12Z)
• Validating Traces of Distributed Programs Against TLA+ Specifications [0.0]
  We present a framework for relating traces of distributed programs to high-level specifications written in TLA+. The problem is reduced to a constrained model checking problem, realized using the TLC model checker. We have applied our approach to several distributed programs, detecting discrepancies between the specifications and the implementations in all cases.
  arXiv  Detail & Related papers  (2024-04-24T01:33:07Z)
• Towards Aligned Layout Generation via Diffusion Model with Aesthetic Constraints [53.66698106829144]
  We propose a unified model to handle a broad range of layout generation tasks. The model is based on continuous diffusion models. Experiment results show that LACE produces high-quality layouts.
  arXiv  Detail & Related papers  (2024-02-07T11:12:41Z)
• Fine-grained Controllable Video Generation via Object Appearance and Context [74.23066823064575]
  We propose fine-grained controllable video generation (FACTOR) to achieve detailed control. FACTOR aims to control objects' appearances and context, including their location and category. Our method achieves controllability of object appearances without finetuning, which reduces the per-subject optimization efforts for the users.
  arXiv  Detail & Related papers  (2023-12-05T17:47:33Z)
• Spreadsheet-based Configuration of Families of Real-Time Specifications [0.0]
  This work exploits variability of the formal model being analysed and the requirements being checked, to facilitate the model-checking of variations of real-time specifications. The configuration of the variability of the formal specifications is described in MS Excel spreadsheets with a particular structure, making it easy to use also by developers. We propose the extension of our previous work by exploiting analysis over valid combination of features, while preserving the simplicity of a spreadsheet-based interface with the model checker.
  arXiv  Detail & Related papers  (2023-10-31T12:16:56Z)
• Requirements Analysis of Variability Constraints in a Configurable Flight Software System [0.0]
  We report on our experience with the variability-related requirements constraints of a flight software framework used by multiple space missions. We propose a new software variability model, similar to a product-line feature model, in the flight software framework.
  arXiv  Detail & Related papers  (2023-09-06T22:56:39Z)
• SSMG: Spatial-Semantic Map Guided Diffusion Model for Free-form Layout-to-Image Generation [68.42476385214785]
  We propose a novel Spatial-Semantic Map Guided (SSMG) diffusion model that adopts the feature map, derived from the layout, as guidance. SSMG achieves superior generation quality with sufficient spatial and semantic controllability compared to previous works. We also propose the Relation-Sensitive Attention (RSA) and Location-Sensitive Attention (LSA) mechanisms.
  arXiv  Detail & Related papers  (2023-08-20T04:09:12Z)
• Adaptive Spot-Guided Transformer for Consistent Local Feature Matching [64.30749838423922]
  We propose Adaptive Spot-Guided Transformer (ASTR) for local feature matching. ASTR models the local consistency and scale variations in a unified coarse-to-fine architecture.
  arXiv  Detail & Related papers  (2023-03-29T12:28:01Z)
• Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
  AuditAI bridges the gap between interpretable formal verification and scalability. We show how AuditAI allows us to obtain controlled variations for verification and certified training while addressing the limitations of verifying using only pixel-space perturbations.
  arXiv  Detail & Related papers  (2021-09-25T22:53:24Z)
• CARE: Coherent Actionable Recourse based on Sound Counterfactual Explanations [0.0]
  This paper introduces CARE, a modular explanation framework that addresses the model- and user-level desiderata. As a model-agnostic approach, CARE generates multiple, diverse explanations for any black-box model.
  arXiv  Detail & Related papers  (2021-08-18T15:26:59Z)
• Unsupervised Learning of General-Purpose Embeddings for Code Changes [6.652641137999891]
  We propose an approach for obtaining embeddings of code changes during pre-training. We evaluate them on two different downstream tasks - applying changes to code and commit message generation. Our model outperforms the model that uses full edit sequences by 5.9 percentage points in accuracy.
  arXiv  Detail & Related papers  (2021-06-03T19:08:53Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.