論文の概要: Validating Traces of Distributed Programs Against TLA+ Specifications
- arxiv url: http://arxiv.org/abs/2404.16075v1
- Date: Wed, 24 Apr 2024 01:33:07 GMT
- ステータス: 処理完了
- システム内更新日: 2024-04-26 18:22:04.747503
- 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 inTLA+. 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 it is not necessary to provide values for all 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, how to interpret the verdict produced by TLC, and how to take into account the results of trace validation for implementation development.
- Abstract(参考訳): TLA+は、分散アルゴリズムを含むシステムを特定するための形式言語であり、強力な検証ツールによってサポートされている。
本稿では,分散プログラムのトレースをTLA+で記述した高レベル仕様に関連付けるためのフレームワークを提案する。
この問題は、TLCモデルチェッカーを用いて実現した制約付きモデルチェック問題に還元される。
我々のフレームワークは,実行のトレースを記録するためにJavaプログラムを計測するAPI,それらのトレースを仕様に関連付けるために使用するTLA+演算子のコレクション,モデルチェッカーを実行するためのスクリプトで構成される。
提案手法を複数の分散プログラムに適用し,すべてのケースにおいて仕様と実装の相違を検出する。
本稿では,これらの相違の原因,TLCによる検証の解釈方法,実装開発におけるトレース検証の結果を考慮する方法について論じる。
関連論文リスト
- Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。
オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。
予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
論文 参考訳(メタデータ) (2023-11-15T14:41:57Z) - 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) - Free Lunch: Robust Cross-Lingual Transfer via Model Checkpoint Averaging [60.79382212029304]
超多言語言語モデルはゼロショット (ZS-XLT) と少数ショット (FS-XLT) の言語間転送において強い性能を示している。
本稿では,タスクの微調整中に異なるチェックポイント(モデルスナップショット)を平均化する,シンプルで効果的な手法を提案する。
論文 参考訳(メタデータ) (2023-05-26T11:24:32Z) - Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
Program-Guided Fact-Checking (ProgramFC)は、複雑なクレームを単純なサブタスクに分解する新しいファクトチェックモデルである。
まず,大規模言語モデルの文脈内学習能力を活用して推論プログラムを生成する。
我々は,各サブタスクを対応するサブタスクハンドラに委譲することでプログラムを実行する。
論文 参考訳(メタデータ) (2023-05-22T06:11:15Z) - Understanding Factual Errors in Summarization: Errors, Summarizers,
Datasets, Error Detectors [105.12462629663757]
本研究では、既存の9つのデータセットから事実性エラーアノテーションを集約し、基礎となる要約モデルに従ってそれらを階層化する。
本稿では,この階層化ベンチマークにおいて,最近のChatGPTベースの指標を含む最先端の事実性指標の性能を比較し,その性能が様々な種類の要約モデルで大きく異なることを示す。
論文 参考訳(メタデータ) (2022-05-25T15:26:48Z) - Task-guided Disentangled Tuning for Pretrained Language Models [16.429787408467703]
本稿では,事前学習型言語モデル(PLM)のためのタスク誘導型ディスタングル型チューニング(TDT)を提案する。
TDTは、タスク関連信号を絡み合った表現から切り離すことにより、表現の一般化を強化する。
GLUE と CLUE のベンチマークによる実験結果から,TDT は異なる PLM を用いた微調整よりも一貫した結果が得られた。
論文 参考訳(メタデータ) (2022-03-22T03:11:39Z) - Towards Dynamic Consistency Checking in Goal-directed Predicate Answer
Set Programming [2.3204178451683264]
本稿では,動的一貫性チェック(Dynamic Consistency check)と呼ばれるトップダウン評価戦略のバリエーションを示す。
これにより、リテラルがプログラムのグローバルな制約に関連する否定と互換性がないかどうかを判断できる。
我々は、標準バージョンのs(CASP)の最大90倍のスピードアップを実験的に観察した。
論文 参考訳(メタデータ) (2021-10-22T20:38:48Z) - Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
AuditAIは、解釈可能な形式検証とスケーラビリティのギャップを埋める。
AuditAIは、画素空間の摂動のみを用いた検証の限界に対処しながら、検証と認定トレーニングのための制御されたバリエーションを得られるかを示す。
論文 参考訳(メタデータ) (2021-09-25T22:53:24Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。