論文の概要: Combining model checking with simulation-based techniques for protocol verification
- arxiv url: http://arxiv.org/abs/2607.17453v1
- Date: Mon, 20 Jul 2026 01:00:20 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-21 18:48:37.470366
- Title: Combining model checking with simulation-based techniques for protocol verification
- Title（参考訳）: プロトコル検証のためのモデルチェックとシミュレーションに基づく手法の併用
- Abstract要約: 本稿では,モデルチェックとシミュレーション関係を組み合わせた手法を提案する。
SCP(Simple Communication Protocol)、ABP(Alternating Bit Protocol)、SWP(Sliding Window Protocol)の3つのプロトコルに焦点を当てる。
- 参考スコア（独自算出の注目度）: 1.6973426830397944
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Model checking is a powerful technique for verifying properties of systems or protocols, but it often suffers from the state space explosion problem. For protocols such as the Alternating Bit Protocol (ABP) and the Sliding Window Protocol (SWP), increasing parameters such as channel capacities or window sizes leads to a reachable state space that is infeasible for exhaustive model checking. To address this, we propose a technique that combines model checking with simulation relations. We focus on three protocols: the Simple Communication Protocol (SCP), ABP, and SWP. Formalized as state machines, these protocols are presented in decreasing order of abstraction: SCP, ABP, and then SWP, which results in a corresponding increase in reachable states. While SCP is verifiable through direct model checking without state space explosion, the direct application of model checking to ABP and SWP becomes infeasible as their parameter values increase. We demonstrate that ABP satisfies its invariant property by combining model checking on SCP with a simulation relation from ABP to SCP. Furthermore, we demonstrate that SWP satisfies its invariant property through the composition of simulation relations from SWP to ABP and from ABP to SCP, in conjunction with model checking on SCP. These approaches enable the formal verification of protocols with large reachable state spaces by conducting model checking on a significantly smaller state machine.
- Abstract（参考訳）: モデル検査はシステムやプロトコルの特性を検証するための強力な手法であるが、しばしば状態空間の爆発的な問題に悩まされる。
Alternating Bit Protocol (ABP) や Sliding Window Protocol (SWP) のようなプロトコルでは、チャネル容量やウィンドウサイズなどのパラメータの増加は、網羅的なモデルチェックでは不可能な到達可能な状態空間につながる。
そこで本研究では,モデル検査とシミュレーション関係を組み合わせた手法を提案する。
我々は,SCP(Simple Communication Protocol),APP,SWPの3つのプロトコルに注目した。
状態機械として形式化されたこれらのプロトコルは、SCP、APP、SWPといった抽象的な順序で表現され、それに応じて到達可能な状態が増加する。
SCPは、状態空間の爆発を伴わない直接モデル検査によって検証できるが、パラメータ値の増大に伴い、APPとSWPへのモデル検査の直接適用は不可能となる。
ABP は,SCP 上のモデルチェックと ABP から SCP へのシミュレーション関係を組み合わせることで,その不変性を満たすことを示した。
さらに,SWP は SWP から ABP および ABP から SCP へのシミュレーション関係を SCP のモデル検査と組み合わせることで,その不変性を満たすことを示した。
これらのアプローチにより、より小さな状態マシン上でモデルチェックを行うことで、大きな到達可能な状態空間を持つプロトコルの正式な検証が可能になる。
関連論文リスト
- A Technical Taxonomy of LLM Agent Communication Protocols [60.76747983053368]
本研究では,大規模言語モデル(LLM)エージェント通信プロトコルの分類と解析を行う技術的分類法を開発する。
このフレームワークはプロトコルの選択をガイドし、プライバシーやポリシー執行といったオープンな研究ギャップを強調する。
論文 参考訳（メタデータ） (2026-06-17T14:45:20Z) - CIAware-Bench: Benchmarking Control Intervention Awareness Across Frontier LLMs [100.38986535324284]
我々は、フロンティアモデル全体でのtextbfcontrol textbfintervention (CI) の認識を測定するベンチマークである textbfCIAware-Bench を紹介する。
CIAware-Benchは、モデルが自身の軌跡を制御介入によって修正されたものと区別できるかどうかをテストする。
論文 参考訳（メタデータ） (2026-06-09T16:24:16Z) - AgentRFC: Security Design Principles and Conformance Testing for Agent Protocols [2.1352949241716352]
エージェントプロトコルにより、自律的なエージェントが機能を発見し、タスクを委譲し、信頼境界を越えてサービスを構成することができる。
大規模なデプロイメントにもかかわらず、これらのプロトコルの体系的なセキュリティフレームワークは存在しない。
Agent Protocol Stack、Agent-Agnostic Security Model、AgentConformの3つのコントリビューションを提示します。
論文 参考訳（メタデータ） (2026-03-25T00:25:02Z) - Model Correlation Detection via Random Selection Probing [62.093777777813756]
既存の類似性に基づく手法では、モデルパラメータにアクセスしたり、しきい値なしでスコアを生成する必要がある。
本稿では,モデル相関検出を統計的テストとして定式化する仮説テストフレームワークであるランダム選択探索(RSP)を紹介する。
RSPは相関の証拠を定量化する厳密なp-値を生成する。
論文 参考訳（メタデータ） (2025-09-29T01:40:26Z) - LLM-Assisted Model-Based Fuzzing of Protocol Implementations [9.512044399020514]
プロトコル動作の障害は脆弱性やシステム障害につながる可能性がある。
プロトコルテストに対する一般的なアプローチは、プロトコルの状態遷移と期待される振る舞いをキャプチャするマルコフモデルを構築することである。
本稿では,大規模言語モデル(LLM)を利用して,ネットワークプロトコルの実装をテストするためのシーケンスを自動的に生成する手法を提案する。
論文 参考訳（メタデータ） (2025-08-03T13:16:18Z) - Towards Semantic Communication Protocols: A Probabilistic Logic
Perspective [69.68769942563812]
我々は,NPMを確率論理型言語ProbLogで記述された解釈可能なシンボルグラフに変換することによって構築された意味プロトコルモデル(SPM)を提案する。
その解釈性とメモリ効率を利用して、衝突回避のためのSPM再構成などのいくつかの応用を実演する。
論文 参考訳（メタデータ） (2022-07-08T14:19:36Z) - Data post-processing for the one-way heterodyne protocol under
composable finite-size security [62.997667081978825]
本研究では,実用的連続可変(CV)量子鍵分布プロトコルの性能について検討する。
ヘテロダイン検出を用いたガウス変調コヒーレント状態プロトコルを高信号対雑音比で検討する。
これにより、プロトコルの実践的な実装の性能を調べ、上記のステップに関連付けられたパラメータを最適化することができる。
論文 参考訳（メタデータ） (2022-05-20T12:37:09Z) - Performance analysis of continuous-variable quantum key distribution
using non-Gaussian states [0.0]
本研究では,連続変数非ガウス状態の離散変調によるプロトコルの効率解析を行う。
我々は、Eveの情報をプロトコルに基づいてバウンドできるという事実を用いて、集団攻撃に対するセキュアな鍵生成率を算出する。
論文 参考訳（メタデータ） (2021-12-19T11:55:17Z) - Lifted Model Checking for Relational MDPs [12.574454799055026]
pCTL-REBELは、リレーショナルMDP上のpCTL特性を検証するためのリフトモデルチェック手法である。
pCTLモデル検査手法は, 無限領域であっても, リレーショナルMDPに対して決定可能であることを示す。
論文 参考訳（メタデータ） (2021-06-22T13:12:36Z) - CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT
(Extended Version) [62.96267257163426]
我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。
まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。
次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
論文 参考訳（メタデータ） (2021-03-18T20:22:50Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。