論文の概要: 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による検証の解釈方法について論じる。
関連論文リスト
- CLOVER: A Test Case Generation Benchmark with Coverage, Long-Context, and Verification [71.34070740261072]
本稿では,テストケースの生成と完成におけるモデルの能力を評価するためのベンチマークCLOVERを提案する。
ベンチマークはタスク間でのコード実行のためにコンテナ化されています。
論文 参考訳（メタデータ） (2025-02-12T21:42:56Z) - TGOSPA Metric Parameters Selection and Evaluation for Visual Multi-object Tracking [4.998475411100799]
トラジェクトリ一般化最適サブパターン割り当て(TGOSPA)を用いて、多目的追跡性能を評価する。
ローカライズエラー、ミスや偽のオブジェクトの数、トラックスイッチの数などが説明できる。
TGOSPAパラメータの選択を探索することにより、特定のタスクに適したアルゴリズムの性能を比較し、理解し、最適化することができる。
論文 参考訳（メタデータ） (2024-12-11T11:57:05Z) - Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast [5.019791860882564]
本稿では,VeriFast で検証可能な C プログラムの仕様作成における OpenAI の GPT-4o モデルの有効性について検討する。
以上の結果から,GPT-4oで生成された仕様は機能的挙動を保っているが,検証に苦慮していることが明らかとなった。
論文 参考訳（メタデータ） (2024-11-04T17:44:11Z) - 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) - TESTEVAL: Benchmarking Large Language Models for Test Case Generation [15.343859279282848]
大規模言語モデル(LLM)を用いたテストケース生成のための新しいベンチマークであるTESTEVALを提案する。
オンラインプログラミングプラットフォームLeetCodeから210のPythonプログラムを収集し、全体的なカバレッジ、ターゲットライン/ブランチカバレッジ、ターゲットパスカバレッジという3つの異なるタスクを設計します。
特定のプログラム行/ブランチ/パスをカバーするテストケースを生成することは、現在のLLMでは依然として困難である。
論文 参考訳（メタデータ） (2024-06-06T22:07:50Z) - Instruction Tuning for Large Language Models: A Survey [52.86322823501338]
我々は、教師付き微調整(SFT)の一般的な方法論を含む、文献の体系的なレビューを行う。
また、既存の戦略の欠陥を指摘しながら、SFTの潜在的な落とし穴についても、それに対する批判とともに検討する。
論文 参考訳（メタデータ） (2023-08-21T15:35:16Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。