論文の概要: 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による検証の解釈方法について論じる。
関連論文リスト
- KAT: Dependency-aware Automated API Testing with Large Language Models [1.7264233311359707]
KAT(Katalon API Testing)は、APIを検証するためのテストケースを自律的に生成する、AI駆動の新たなアプローチである。
実世界の12のサービスを用いたKATの評価は、検証カバレッジを改善し、文書化されていないステータスコードを検出し、これらのサービスの偽陽性を低減できることを示している。
論文 参考訳(メタデータ) (2024-07-14T14:48:18Z) - Concurrent Linguistic Error Detection (CLED) for Large Language Models [13.01669288397494]
大規模言語モデル(LLM)に対する同時言語誤り検出(CLED)を提案する。
CLEDはLLMによって生成されたテキストの言語的特徴を抽出し、エラーを検出する同時分類器に供給する。
提案手法は,ニュース要約時にT5モデル,翻訳時にOPUS-MTモデルで評価されている。
論文 参考訳(メタデータ) (2024-03-25T03:17:27Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。