Fugu-MT 論文翻訳(概要): Multi-Grained Specifications for Distributed System Model Checking and Verification

論文の概要: Multi-Grained Specifications for Distributed System Model Checking and Verification

arxiv url: http://arxiv.org/abs/2409.14301v3
Date: Fri, 27 Sep 2024 08:15:53 GMT
ステータス: 処理完了
システム内更新日: 2024-11-06 23:15:03.799579
Title: Multi-Grained Specifications for Distributed System Model Checking and Verification
Title（参考訳）: 分散システムモデルチェックと検証のためのマルチグレード仕様
Authors: Lingzhi Ouyang, Xudong Sun, Ruize Tang, Yu Huang, Madhav Jivrajani, Xiaoxing Ma, Tianyin Xu,
Abstract要約: 我々はTLA+を用いて、ZooKeeperとTLCモデルチェッカーのきめ細かい挙動をモデル化し、その正確性を検証する。複数きめの仕様を書くことは現実的な実践であり、不安定な状態空間を伴わずにモデルコードギャップに対処できることを示す。
参考スコア（独自算出の注目度）: 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.
Abstract（参考訳）: 本稿では,複雑な分散コーディネーションシステムであるZooKeeperの正当性を特定し,検証した。我々は、ZooKeeperのきめ細かい振る舞いをモデル化するためにTLA+を使用し、TLCモデルチェッカーを使用してその正しさ特性を検証する。基本的な課題は、仕様の粒度とモデルチェックのスケーラビリティのバランスをとることです -- きめ細かい仕様は、状態空間の爆発を引き起こします。この課題に対処するため、構成可能なモジュールの粒度が異なる仕様を作成し、特定のシナリオに基づいてそれらを混合した仕様に構成する。例えば、コードの変更を検証するために、変更したモジュールのきめ細かい仕様と、変更されていないコードの詳細を保存されたインタラクションで抽象化する粗い仕様を作成します。多粒度仕様を書くことは実行可能なプラクティスであり、特に変更が通常ローカルでインクリメンタルなソフトウェアを進化させるためには、状態空間を保たずにモデルコードギャップに対処できることを示します。 5種類の不変性に反する6つの重大なバグを検出し、そのコード修正を確認しました。また、プロトコル設計を改善して、正しく実装できるようにしています。

関連論文リスト

Multi-Convformer: Extending Conformer with Multiple Convolution Kernels [64.4442240213399]
我々は,マルチコンバータを導入し,複数のコンバータカーネルをゲーティングと合わせてコンバータの畳み込みモジュール内で利用する。我々のモデルは、よりパラメータ効率の良いCgMLPやE-Branchformerといった既存のConformerと性能的に競合する。我々は4つの異なるデータセットと3つの異なるモデリングパラダイムにまたがって、我々のアプローチをConformerとその変種と経験的に比較し、最大8%の相対的な単語誤り率(WER)の改善を示す。
論文参考訳（メタデータ） (2024-07-04T08:08:12Z)
Validating Traces of Distributed Programs Against TLA+ Specifications [0.0]
本稿では,分散プログラムのトレースをTLA+で記述された高レベル仕様に関連付けるためのフレームワークを提案する。この問題は、TLCモデルチェッカーを用いて実現した制約付きモデルチェック問題に還元される。提案手法を複数の分散プログラムに適用し,すべてのケースにおいて仕様と実装の相違を検出する。
論文参考訳（メタデータ） (2024-04-24T01:33:07Z)
Towards Aligned Layout Generation via Diffusion Model with Aesthetic Constraints [53.66698106829144]
広い範囲のレイアウト生成タスクを処理する統一モデルを提案する。このモデルは連続拡散モデルに基づいている。実験結果から,LACEは高品質なレイアウトを生成することがわかった。
論文参考訳（メタデータ） (2024-02-07T11:12:41Z)
Fine-grained Controllable Video Generation via Object Appearance and Context [74.23066823064575]
細粒度制御可能なビデオ生成法(FACTOR)を提案する。 FACTORは、オブジェクトの位置とカテゴリを含む、オブジェクトの外観とコンテキストを制御することを目的としている。本手法は,オブジェクトの外観を微調整せずに制御し,オブジェクトごとの最適化作業を省く。
論文参考訳（メタデータ） (2023-12-05T17:47:33Z)
Spreadsheet-based Configuration of Families of Real-Time Specifications [0.0]
この作業は、分析される形式モデルと、検査される要件の変動を利用して、リアルタイム仕様のバリエーションのモデルチェックを容易にする。形式仕様のバリエーションの設定は、特定の構造を持つMS Excelスプレッドシートで記述されており、開発者が簡単に使用することができる。本稿では,スプレッドシートベースのインタフェースとモデルチェッカーのシンプルさを保ちながら,機能の組み合わせを解析的に活用して,これまでの作業の拡張を提案する。
論文参考訳（メタデータ） (2023-10-31T12:16:56Z)
Requirements Analysis of Variability Constraints in a Configurable Flight Software System [0.0]
複数の宇宙ミッションで使用される飛行ソフトウェアフレームワークの変動性に関する要件制約について報告する。本研究では,フライトソフトウェアフレームワークにおいて,製品ライン機能モデルに似た新しいソフトウェア変数モデルを提案する。
論文参考訳（メタデータ） (2023-09-06T22:56:39Z)
SSMG: Spatial-Semantic Map Guided Diffusion Model for Free-form Layout-to-Image Generation [68.42476385214785]
本稿では,レイアウトから派生した特徴写像を用いた空間意味マップガイド(SSMG)拡散モデルを提案する。 SSMGは,従来の研究に比べて空間的,意味的な制御性に優れた生成品質を実現する。また,RSA(Relation-Sensitive Attention)機構とLSA(Location-Sensitive Attention)機構を提案する。
論文参考訳（メタデータ） (2023-08-20T04:09:12Z)
Adaptive Spot-Guided Transformer for Consistent Local Feature Matching [64.30749838423922]
局所的特徴マッチングのための適応スポットガイド変換器(ASTR)を提案する。 ASTRは、統一された粗いアーキテクチャにおける局所的な一貫性とスケールのバリエーションをモデル化する。
論文参考訳（メタデータ） (2023-03-29T12:28:01Z)
Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
AuditAIは、解釈可能な形式検証とスケーラビリティのギャップを埋める。 AuditAIは、画素空間の摂動のみを用いた検証の限界に対処しながら、検証と認定トレーニングのための制御されたバリエーションを得られるかを示す。
論文参考訳（メタデータ） (2021-09-25T22:53:24Z)
CARE: Coherent Actionable Recourse based on Sound Counterfactual Explanations [0.0]
本稿では,モデルおよびユーザレベルのデシダータに対処するモジュール型説明フレームワークであるCAREを紹介する。モデルに依存しないアプローチとして、CAREはブラックボックスモデルに対して複数の多様な説明を生成する。
論文参考訳（メタデータ） (2021-08-18T15:26:59Z)
Unsupervised Learning of General-Purpose Embeddings for Code Changes [6.652641137999891]
事前学習中にコード変更の埋め込みを得る手法を提案する。コードの変更とコミットメッセージ生成という、2つの異なる下流タスクでそれらを評価します。本モデルでは,完全編集シーケンスを用いたモデルの精度を5.9ポイント向上させる。
論文参考訳（メタデータ） (2021-06-03T19:08:53Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。