論文の概要: Validating Traces of Distributed Programs Against TLA+ Specifications
- arxiv url: http://arxiv.org/abs/2404.16075v2
- Date: Tue, 17 Sep 2024 16:52:15 GMT
- ステータス: 処理完了
- システム内更新日: 2024-09-18 22:10:43.471411
- Title: Validating Traces of Distributed Programs Against TLA+ Specifications
- Title（参考訳）: TLA+仕様に対する分散プログラムのトレースの検証
- Authors: Horatiu Cirstea, Markus A. Kuppe, Benjamin Loillier, Stephan Merz,
- Abstract要約: 本稿では,分散プログラムのトレースをTLA+で記述された高レベル仕様に関連付けるためのフレームワークを提案する。
この問題は、TLCモデルチェッカーを用いて実現した制約付きモデルチェック問題に還元される。
提案手法を複数の分散プログラムに適用し,すべてのケースにおいて仕様と実装の相違を検出する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: TLA+ is a formal language for specifying systems, including distributed algorithms, that is supported by powerful verification tools. In this work 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. Our framework consists of an API for instrumenting Java programs in order to record traces of executions, of a collection of TLA+ operators that are used for relating those traces to specifications, and of scripts for running the model checker. Crucially, traces only contain updates to specification variables rather than full values, and developers may choose to trace only certain variables. We have applied our approach to several distributed programs, detecting discrepancies between the specifications and the implementations in all cases. We discuss reasons for these discrepancies, best practices for instrumenting programs, and how to interpret the verdict produced by TLC.
- Abstract（参考訳）: TLA+は、分散アルゴリズムを含むシステムを特定するための形式言語であり、強力な検証ツールによってサポートされている。
本稿では,分散プログラムのトレースをTLA+で記述された高レベル仕様に関連付けるためのフレームワークを提案する。
この問題は、TLCモデルチェッカーを用いて実現した制約付きモデルチェック問題に還元される。
我々のフレームワークは,Javaプログラムを計測して実行のトレースを記録するAPI,それらのトレースを仕様に関連付けるために使用されるTLA+演算子のコレクション,モデルチェッカーを実行するためのスクリプトで構成される。
重要なのは、トレースには完全な値ではなく、仕様変数のアップデートのみが含まれており、開発者は特定の変数だけをトレースする選択をすることができる。
提案手法を複数の分散プログラムに適用し,すべてのケースにおいて仕様と実装の相違を検出する。
本稿では,これらの不一致の原因,計測プログラムのベストプラクティス,TLCによる検証の解釈方法について論じる。
関連論文リスト
- SpecTool: A Benchmark for Characterizing Errors in Tool-Use LLMs [77.79172008184415]
SpecToolは、ツール使用タスクのLLM出力のエラーパターンを特定するための新しいベンチマークである。
もっとも顕著なLCMでも,これらの誤りパターンが出力に現れることを示す。
SPECTOOLの分析と洞察を使って、エラー軽減戦略をガイドすることができる。
論文 参考訳（メタデータ） (2024-11-20T18:56:22Z) - Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast [5.019791860882564]
大規模言語モデル(LLM)は、多くのソフトウェアエンジニアリング活動において有望であることを示している。
本稿では,分離論理に基づく仕様生成におけるOpenAIのGPTモデルの有効性について検討する。
論文 参考訳（メタデータ） (2024-11-04T17:44:11Z) - DiffSpec: Differential Testing with LLMs using Natural Language Specifications and Code Artifacts [6.222103009114668]
大規模な言語モデルで差分テストを生成するためのフレームワークであるDiffSpecを紹介する。
本稿では,2つの異なるシステム,すなわちeBPFランタイムとWasmバリデータに対するDiffSpecの有効性を示す。
論文 参考訳（メタデータ） (2024-10-05T18:11:14Z) - Multi-Grained Specifications for Distributed System Model Checking and Verification [9.14614889088682]
我々はTLA+を用いて、ZooKeeperとTLCモデルチェッカーのきめ細かい挙動をモデル化し、その正確性を検証する。
複数きめの仕様を書くことは現実的な実践であり、不安定な状態空間を伴わずにモデルコードギャップに対処できることを示す。
論文 参考訳（メタデータ） (2024-09-22T02:59:56Z) - Fine-Tuning with Divergent Chains of Thought Boosts Reasoning Through Self-Correction in Language Models [63.36637269634553]
本稿では,複数の推論連鎖を比較するためにモデルを必要とすることによって,性能を向上する新しい手法を提案する。
DCoTデータセットの命令チューニングにより、より小さく、よりアクセスしやすい言語モデルの性能が向上することがわかった。
論文 参考訳（メタデータ） (2024-07-03T15:01:18Z) - Disperse-Then-Merge: Pushing the Limits of Instruction Tuning via Alignment Tax Reduction [75.25114727856861]
大規模言語モデル(LLM)は、スーパービジョンされた微調整プロセスの後半で劣化する傾向にある。
この問題に対処するための単純な分散結合フレームワークを導入する。
我々のフレームワークは、一連の標準知識と推論ベンチマークに基づいて、データキュレーションや正規化の訓練など、様々な高度な手法より優れています。
論文 参考訳（メタデータ） (2024-05-22T08:18:19Z) - Requirements Traceability: Recovering and Visualizing Traceability Links
Between Requirements and Source Code of Object-oriented Software Systems [0.0]
要求からコードへのトレーサビリティリンク(RtC-TL)は、要求とソースコードのアーティファクトの関係を形作る。
本稿では、RtC-TLの復元と可視化のための自動アプローチと実装であるYamenTraceを紹介する。
論文 参考訳（メタデータ） (2023-07-09T11:01:16Z) - Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
Program-Guided Fact-Checking (ProgramFC)は、複雑なクレームを単純なサブタスクに分解する新しいファクトチェックモデルである。
まず,大規模言語モデルの文脈内学習能力を活用して推論プログラムを生成する。
我々は,各サブタスクを対応するサブタスクハンドラに委譲することでプログラムを実行する。
論文 参考訳（メタデータ） (2023-05-22T06:11:15Z) - Fault-Aware Neural Code Rankers [64.41888054066861]
サンプルプログラムの正しさを予測できる故障認識型ニューラルネットワークローダを提案する。
我々のフォールト・アウェア・ローダは、様々なコード生成モデルのpass@1精度を大幅に向上させることができる。
論文 参考訳（メタデータ） (2022-06-04T22:01:05Z) - Self-Supervised Log Parsing [59.04636530383049]
大規模ソフトウェアシステムは、大量の半構造化ログレコードを生成する。
既存のアプローチは、ログ特化や手動ルール抽出に依存している。
本稿では,自己教師付き学習モデルを用いて解析タスクをマスク言語モデリングとして定式化するNuLogを提案する。
論文 参考訳（メタデータ） (2020-03-17T19:25:25Z) - Learning to Encode and Classify Test Executions [14.67675979776677]
本論文の目的は,一般的な,スケーラブルで高精度なテストオラクル問題を解くことである。
実行トレースのごく一部をパスまたはフェールの判定でラベル付けします。
ラベル付きトレースを使用して、ニューラルネットワーク(NN)モデルをトレーニングし、実行のパスとフェールを区別する実行パターンを学習します。
論文 参考訳（メタデータ） (2020-01-08T10:53:45Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。