論文の概要: Systematic API Testing Through Model Checking and Executable Contracts

• arxiv url: http://arxiv.org/abs/2604.08633v1
• Date: Thu, 09 Apr 2026 17:00:42 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-13 17:57:53.507911
• Title: Systematic API Testing Through Model Checking and Executable Contracts
• Title（参考訳）: モデルチェックと実行可能なコントラクトによるシステマティックAPIテスト
• Abstract要約: モデルチェックを活用することで,APIテストの体系的な状態空間カバレッジを実現するフレームワークであるIcePickを紹介した。 IcePickはTLA+を使用して、API状態の進化を正式にモデル化し、TLCモデルチェッカーを使用して、到達可能な状態を徹底的に探索し、振る舞いモデルを確実にカバーするテストシーケンスを生成する。 HTTPステータスコード以外のオラクル制限に対処するために、API仕様を実行可能なセマンティックコントラクトで強化する一階述語論理コントラクト言語であるGlacierを提案する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated black-box testing of APIs typically relies on interface specifications that define available operations and data schemas, but offer limited or no behavioural semantics. This semantic gap amplifies the test-oracle problem and limits the generation of effective, stateful call sequences. We introduce IcePick, a framework that achieves systematic state-space coverage for API testing by leveraging model checking. IcePick uses TLA+ to formally model API state evolution, employs the TLC model checker to exhaustively explore reachable states, and generates test sequences that provably cover the behavioural model. To mitigate state-space explosion and improve sequence extraction, we introduce a coverage-guided breadth-first traversal of the TLC state-space graph. To address oracle limitations beyond HTTP status codes, we propose Glacier, a first-order logic contract language that enriches API specifications with executable semantic contracts, enabling automated behavioural verification during test execution. We evaluate IcePick on EvoMaster Benchmark systems, demonstrating that model-checking-guided exploration achieves complete state coverage and reveals faults in multi-operation interactions. We also analyse scalability to characterise practical limits and applicability requirements. Overall, IcePick provides reproducible test suites with strong coverage guarantees for critical API-based systems.
• Abstract（参考訳）: APIの自動ブラックボックステストは、一般的に利用可能な操作とデータスキーマを定義するインターフェース仕様に依存しますが、限定的、あるいは振る舞いのセマンティクスを提供していません。 このセマンティックギャップは、テストラクル問題を増幅し、有効でステートフルな呼び出しシーケンスの生成を制限する。 モデルチェックを活用することで,APIテストの体系的な状態空間カバレッジを実現するフレームワークであるIcePickを紹介した。 IcePickはTLA+を使用して、API状態の進化を正式にモデル化し、TLCモデルチェッカーを使用して、到達可能な状態を徹底的に探索し、振る舞いモデルを確実にカバーするテストシーケンスを生成する。 状態空間の爆発を緩和し、シーケンス抽出を改善するため、TLC状態空間グラフのカバレッジ誘導の第1トラバースを導入する。 HTTPステータスコード以外のオラクル制限に対処するために、API仕様を実行可能なセマンティックコントラクトで強化し、テスト実行中の自動振る舞い検証を可能にする一階述語論理コントラクト言語であるGlacierを提案する。 我々は、EvoMaster Benchmarkシステム上でIcePickを評価し、モデルチェック誘導探索が完全な状態カバレッジを実現し、マルチオペレーションインタラクションにおける欠陥を明らかにすることを実証した。 また、スケーラビリティを分析して、実用的限界と適用性要件を特徴づけます。 全体として、IcePickは、重要なAPIベースのシステムに対して、強力なカバレッジ保証を備えた再現可能なテストスイートを提供する。

関連論文リスト

• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  大規模言語モデル(LLM)によって駆動されるエージェントシステムは、永続的な運用データを扱う現実世界にますます展開されている。 既存のアプローチはそのようなシステムレベルの保証を提供していません。 本稿では, 1 つの LLM とツールオーケストレーションハーネスからなるエージェントシステムのリレーショナル操作データに対する検証について述べる。
  論文  参考訳（メタデータ） (2026-08-04T13:01:30Z)
• From Resource Flow to Executable Tests: Petri-Net-Guided LLM Test Generation for Concurrent Stateful Rust APIs [5.064868362565062]
  コンカレントステートフルライブラリAPIは、リソースオーナシップの進化、ライフサイクル状態、競合するインターリーブを通じて、振る舞いを公開する。 大規模な言語モデルは実行可能なRustテストを合成できるが、その出力はAPIの前提条件に違反したり、浅いままだったり、偶然のトレースを減らしたりすることが多い。 本稿では,形式的なシナリオ設計と低コストなテストクリエティゼーションのギャップについて論じる。
  論文  参考訳（メタデータ） (2026-07-23T17:15:53Z)
• PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
  我々は、スケジューリング、検証、メモリ、ベンチマーク、安全性をシステムレベルのサービスとして提供するPhyAgentOSを紹介します。 セッション中心のセッションは、スケジューリング、互換性、監督された実行、エビデンス収集、受け入れの最小単位として、アクションではなくセッションを扱う。 SessionVerifierは、実行終了とセマンティックタスク完了を、成功、失敗、または再計画のエビデンスに基づいて判断する。 ベンチマークはデプロイメントセッションと検証パスを再利用するので、結果は実際の実行に遡る。
  論文  参考訳（メタデータ） (2026-07-18T04:46:53Z)
• What to Test Next: Interpretable Coverage Gap Discovery in Driving VLMs [52.50210189669399]
  視覚言語モデル(VLM)を駆動するには,操作設計領域(ODD)が定義する様々な条件のシーンを正確に理解する必要がある SliceScorerは、欠落したスライス推薦のための決定論的スコアリングルールである。 SliceNavは, 従来のスライス発見法よりも, 高リスクカバレッジギャップを効果的に表面化することを示す。
  論文  参考訳（メタデータ） (2026-06-01T03:18:01Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• Combining Static and Dynamic Approaches for Mining and Testing Constraints for RESTful API Testing [10.13889120511225]
  本稿では,新しい静的解析手法(APIレスポンスボディの制約をAPI仕様から抽出する)と動的アプローチを組み合わせることを提案する。 大きな言語モデル(LLM)を活用して、API仕様を理解し、レスポンスボディの制約をマイニングし、テストケースを生成します。 また、生成されたテストケースを使用して、実世界の8つのAPIに対して、API仕様と実際のレスポンスデータとの間の21のミスマッチを検出します。
  論文  参考訳（メタデータ） (2025-04-24T06:28:18Z)
• Test Amplification for REST APIs via Single and Multi-Agent LLM Systems [1.6499388997661122]
  既存のREST APIテストスイートを増幅するために,単一エージェントとマルチエージェントのセットアップである大規模言語モデル(LLM)システムについて検討する。 本稿では, テストカバレッジ, バグ検出の有効性, 計算コストやエネルギー使用量など, 様々な側面における2つのアプローチの比較検討を行う。
  論文  参考訳（メタデータ） (2025-04-10T20:19:50Z)
• Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [71.7892165868749]
  LLM(Commercial Large Language Model) APIは基本的な信頼の問題を生み出します。 ユーザーは特定のモデルに課金するが、プロバイダが忠実に提供できることを保証することはない。 我々は,このモデル置換問題を定式化し,現実的な逆条件下での検出方法を評価する。 我々は,信頼された実行環境(TEE)を実用的で堅牢なソリューションとして使用し,評価する。
  論文  参考訳（メタデータ） (2025-04-07T03:57:41Z)
• Utilizing API Response for Test Refinement [2.8002188463519944]
  本稿では,応答メッセージを利用した動的テスト改善手法を提案する。 インテリジェントエージェントを使用すると、テストシナリオを生成するためにさらに使用されるAPI仕様に制約が追加される。 提案されたアプローチは、4xxレスポンスの数を減少させ、より現実的なテストケースを生成するための一歩を踏み出した。
  論文  参考訳（メタデータ） (2025-01-30T05:26:32Z)
• LlamaRestTest: Effective REST API Testing with Small Language Models [50.058600784556816]
  LlamaRestTestは、2つのLLM(Large Language Models)を使って現実的なテストインプットを生成する新しいアプローチである。 私たちは、GPTを使った仕様強化ツールであるRESTGPTなど、最先端のREST APIテストツールに対して、これを評価しています。 私たちの研究は、REST APIテストにおいて、小さな言語モデルは、大きな言語モデルと同様に、あるいは、より良く機能することができることを示しています。
  論文  参考訳（メタデータ） (2025-01-15T05:51:20Z)
• DeepREST: Automated Test Case Generation for REST APIs Exploiting Deep Reinforcement Learning [5.756036843502232]
  本稿では、REST APIを自動テストするための新しいブラックボックスアプローチであるDeepRESTを紹介します。 深い強化学習を活用して、暗黙のAPI制約、すなわちAPIドキュメントから隠された制約を明らかにする。 実験により,提案手法は高いテストカバレッジと故障検出を実現する上で極めて有効であることが示唆された。
  論文  参考訳（メタデータ） (2024-08-16T08:03:55Z)
• FANTAstic SEquences and Where to Find Them: Faithful and Efficient API Call Generation through State-tracked Constrained Decoding and Reranking [57.53742155914176]
  APIコール生成は、大規模言語モデルのツール使用能力の基盤となっている。 既存の教師付きおよびコンテキスト内学習アプローチは、高いトレーニングコスト、低いデータ効率、APIドキュメントとユーザの要求に反する生成APIコールに悩まされる。 本稿では,これらの制約に対処するため,FANTASEと呼ばれる出力側最適化手法を提案する。
  論文  参考訳（メタデータ） (2024-07-18T23:44:02Z)
• 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)
• Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
  AuditAIは、解釈可能な形式検証とスケーラビリティのギャップを埋める。 AuditAIは、画素空間の摂動のみを用いた検証の限界に対処しながら、検証と認定トレーニングのための制御されたバリエーションを得られるかを示す。
  論文  参考訳（メタデータ） (2021-09-25T22:53:24Z)
• Complex Event Forecasting with Prediction Suffix Trees: Extended Technical Report [70.7321040534471]
  複合イベント認識(CER)システムは、イベントのリアルタイムストリーム上のパターンを"即時"検出する能力によって、過去20年間に人気が高まっている。 このような現象が実際にCERエンジンによって検出される前に、パターンがいつ発生するかを予測する方法が不足している。 複雑なイベント予測の問題に対処しようとする形式的なフレームワークを提案する。
  論文  参考訳（メタデータ） (2021-09-01T09:52:31Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。