論文の概要: Annotating Control-Flow Graphs for Formalized Test Coverage Criteria
- arxiv url: http://arxiv.org/abs/2407.04144v1
- Date: Thu, 4 Jul 2024 20:13:03 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-07-08 15:10:29.194389
- Title: Annotating Control-Flow Graphs for Formalized Test Coverage Criteria
- Title(参考訳): 定式化テストカバレッジ基準に対する制御フローグラフのアノテート
- Abstract要約: 制御フローグラフにグラフ自体から推測される決定情報をアノテートする方法を示す。
我々は,一般的なコンパイラから出力されるCFGを自動的にアノテートするツールとして,アルゴリズムを実装した。
- 参考スコア(独自算出の注目度): 0.3277163122167433
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Control flow coverage criteria are an important part of the process of qualifying embedded software for safety-critical systems. Criteria such as modified condition/decision coverage (MC/DC) as defined by DO-178B are used by regulators to judge the adequacy of testing and by QA engineers to design tests when full path coverage is impossible. Despite their importance, these coverage criteria are often misunderstood. One problem is that their definitions are typically written in natural language specification documents, making them imprecise. Other works have proposed formal definitions using binary predicate logic, but these definitions are difficult to apply to the analysis of real programs. Control-Flow Graphs (CFGs) are the most common model for analyzing program logic in compilers, and seem to be a good fit for defining and analyzing coverage criteria. However, CFGs discard the explicit concept of a decision, making their use for this task seem impossible. In this paper, we show how to annotate a CFG with decision information inferred from the graph itself. We call this annotated model a Control-Flow Decision Graph (CFDG) and we use it to formally define several common coverage criteria. We have implemented our algorithms in a tool which we show can be applied to automatically annotate CFGs output from popular compilers.
- Abstract(参考訳): 制御フローカバレッジ基準は、組込みソフトウェアを安全クリティカルシステムに適合させるプロセスにおいて重要な部分である。
DO-178Bが定義した修正条件/決定カバレッジ(MC/DC)のような基準は、テストの妥当性を判断するために規制当局が、完全なパスカバレッジが不可能な場合にはQAエンジニアがテストの設計を行うために使用される。
その重要性にもかかわらず、これらのカバレッジ基準はしばしば誤解される。
一つの問題は、それらの定義が典型的には自然言語の仕様文書で書かれており、不正確であることである。
他の研究では二進述語論理を用いた形式的定義が提案されているが、これらの定義は実プログラムの分析に適用することは困難である。
制御フローグラフ(CFG)は、コンパイラのプログラムロジックを解析するための最も一般的なモデルであり、カバレッジ基準を定義し、分析するのに適しているように思われる。
しかし、CFGは決定の明示的な概念を捨て、このタスクに使用することは不可能に思える。
本稿では,このグラフから推定される決定情報を用いてCFGにアノテートする方法を示す。
我々はこの注釈付きモデルをCFDG(Control-Flow Decision Graph)と呼び、いくつかの一般的なカバレッジ基準を正式に定義するために使用します。
我々は,一般的なコンパイラから出力されるCFGを自動的にアノテートするツールとして,アルゴリズムを実装した。
関連論文リスト
- AspisAI: A Canonical, Machine-Interpretable Governance Framework for Automated Multi-Standard Compliance Monitoring [0.0]
本稿では,選択した要件を標準的機械解釈制御モデルに変換する,限定的で標準に依存しないガバナンスフレームワークであるemphAspisAIを提案する。
26の代表的な要件の範囲内において、このフレームワークは5つのガバナンス指向の基準に対して制御されたシミュレーションで評価される。
その結果は、完全な要求エンコーディング、88.5,%マッピングカバレッジ、完全なトレーサビリティ、導入されたすべてのギャップの正確な検出を含む。
論文 参考訳(メタデータ) (2026-09-09T22:37:12Z) - Grounded Normative Rule Generation with Structured Search [47.28595196084396]
基底ノルム規則合成(GNRS)として問題を定式化する。
GNRS-SearchはMarkov Chain Monte Carlo(MCMC)サンプリングを利用して、離散5スロットアンドオーグラフ(AOG)を最適化するフレームワークである。
GNRS-Benchは8つのシーンにまたがる116の制御目標にまたがるベンチマークであり、RealCharterBenchは53のリアルなポリシータスクに隠れたソース節で遷移を評価する。
論文 参考訳(メタデータ) (2026-08-23T05:43:42Z) - Structuring Semantic Embeddings for Principle Evaluation: A Prototype-Guided Contrastive Learning Approach [58.15427952222424]
汎用的なテキスト埋め込みはそのようなタスクに広くデプロイされているが、意味的類似性は意味的に似ているがタスク固有の例を示すことができる。
本稿では,凍結したテキスト埋め込み上に構築された幾何正規化モジュールであるPGCL(Prototype-Guided Contrastive Learning)を紹介する。
論文 参考訳(メタデータ) (2026-08-15T13:19:25Z) - Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
大規模言語モデル(LLM)によって駆動されるエージェントシステムは、永続的な運用データを扱う現実世界にますます展開されている。
既存のアプローチはそのようなシステムレベルの保証を提供していません。
本稿では, 1 つの LLM とツールオーケストレーションハーネスからなるエージェントシステムのリレーショナル操作データに対する検証について述べる。
論文 参考訳(メタデータ) (2026-08-04T13:01:30Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳(メタデータ) (2026-05-02T11:31:33Z) - Graph-KV: Breaking Sequence via Injecting Structural Biases into Large Language Models [63.64507678113921]
構造的帰納バイアスを通して相互作用を管理するグラフ-KVを導入する。
このフレームワークでは、「ターゲット」セグメントは指定された「ソース」セグメントのKV-cacheのみに選択的に参加する。
我々は,(1)直接推論,マルチホップ推論,長期文書理解にまたがる7つのRAGベンチマーク,(2)引用エゴグラフとして構造化された全文科学論文を用いた新しい学術論文QAタスクArxiv-QA,(3)引用ネットワーク内の論文トピック分類の3つのシナリオでグラフ-KVを評価する。
論文 参考訳(メタデータ) (2025-06-09T00:30:08Z) - Respecting Temporal-Causal Consistency: Entity-Event Knowledge Graphs for Retrieval-Augmented Generation [69.45495166424642]
我々は,物語文書における時間的,因果的,文字的整合性を理解するために,頑健で差別的なQAベンチマークを開発する。
次に、バイナリマッピングでリンクされたエンティティとイベントのサブグラフを分離したまま保持するデュアルグラフフレームワークであるEntity-Event RAG(E2RAG)を紹介します。
ChronoQA全体で、我々のアプローチは最先端の非構造化およびKGベースのRAGベースラインよりも優れており、因果一貫性クエリや文字整合性クエリが顕著である。
論文 参考訳(メタデータ) (2025-06-06T10:07:21Z) - LogiCase: Effective Test Case Generation from Logical Description in Competitive Programming [7.726159311658054]
CCFG(Context-Free Grammars with Counters)は、入力仕様における構文構造と意味構造の両方をキャプチャする形式である。
微調整のCodeT5モデルを用いて、自然言語入力仕様をCFGに変換し、高品質なテストケースを体系的に生成する。
論文 参考訳(メタデータ) (2025-05-21T02:48:01Z) - SEOE: A Scalable and Reliable Semantic Evaluation Framework for Open Domain Event Detection [70.23196257213829]
オープンドメインイベント検出のためのスケーラブルで信頼性の高いセマンティックレベルの評価フレームワークを提案する。
提案フレームワークはまず,現在7つの主要ドメインをカバーする564のイベントタイプを含む,スケーラブルな評価ベンチマークを構築した。
次に,大言語モデル(LLM)を自動評価エージェントとして活用し,意味的類似ラベルのきめ細かい定義を取り入れた意味的F1スコアを計算する。
論文 参考訳(メタデータ) (2025-03-05T09:37:05Z) - Modified Condition/Decision Coverage in the GNU Compiler Collection [0.0]
GCC 14におけるマスキング修正条件/決定カバレッジ(MC/DC)サポートの実装について述べる。
バイナリ決定図を解析することにより、MC/DCの重要な特性、結果に独立して影響を与える力、制御フローグラフのエッジにマップすることができる。
論文 参考訳(メタデータ) (2025-01-03T22:59:38Z) - CoGS: Model Agnostic Causality Constrained Counterfactual Explanations using goal-directed ASP [1.5749416770494706]
CoGSはモデルに依存しないフレームワークであり、分類モデルの反実的な説明を生成することができる。
CoGSは、望ましい結果を達成するために必要な変更について、解釈可能かつ実行可能な説明を提供する。
論文 参考訳(メタデータ) (2024-10-30T00:43:01Z) - Verifying Non-friendly Formal Verification Designs: Can We Start Earlier? [2.1626093085892144]
本稿では,2つの主要なステップからなるメタモデリング技術に基づく自動手法を提案する。
まず、C++で書かれた未使用のアルゴリズム記述を、生成されたアサーションを使用して早期に検証する。
第2に、HLECとそのメタモデルパラメータを用いて、このアルゴリズム記述をシーケンシャルな設計に対して検証する。
論文 参考訳(メタデータ) (2024-10-24T06:09:40Z) - Automatically Adaptive Conformal Risk Control [49.95190019041905]
本稿では,テストサンプルの難易度に適応して,統計的リスクの近似的条件制御を実現する手法を提案する。
我々のフレームワークは、ユーザが提供するコンディショニングイベントに基づく従来のコンディショニングリスク制御を超えて、コンディショニングに適した関数クラスのアルゴリズム的、データ駆動決定を行う。
論文 参考訳(メタデータ) (2024-06-25T08:29:32Z) - Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
本稿では,検証対応言語における仕様の質を評価するための指標を提案する。
MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。
また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
論文 参考訳(メタデータ) (2024-06-14T06:52:08Z) - Scalable Defect Detection via Traversal on Code Graph [10.860910384163892]
グラフベースの静的解析プラットフォームであるQVoGを導入し、欠陥や脆弱性を検出する。
合理的なグラフサイズを維持するために圧縮されたCPG表現を使用し、それによって全体的なクエリ効率が向上する。
1000,000行以上のコードからなるプロジェクトでは、QVoGはコードQLで19分ではなく、およそ15分で分析を完了できる。
論文 参考訳(メタデータ) (2024-06-12T11:24:52Z) - ProTeCt: Prompt Tuning for Taxonomic Open Set Classification [59.59442518849203]
分類学的オープンセット(TOS)設定では、ほとんどショット適応法はうまくいきません。
本稿では,モデル予測の階層的一貫性を校正する即時チューニング手法を提案する。
次に,階層整合性のための新しいPrompt Tuning(ProTeCt)手法を提案し,ラベル集合の粒度を分類する。
論文 参考訳(メタデータ) (2023-06-04T02:55:25Z) - Pointwise Feasibility of Gaussian Process-based Safety-Critical Control
under Model Uncertainty [77.18483084440182]
制御バリア関数(CBF)と制御リアプノフ関数(CLF)は、制御システムの安全性と安定性をそれぞれ強化するための一般的なツールである。
本稿では, CBF と CLF を用いた安全クリティカルコントローラにおいて, モデル不確実性に対処するためのガウスプロセス(GP)に基づくアプローチを提案する。
論文 参考訳(メタデータ) (2021-06-13T23:08:49Z) - An Efficient Diagnosis Algorithm for Inconsistent Constraint Sets [68.8204255655161]
過制約問題における最小限の障害制約を識別する分割・分散型診断アルゴリズム(FastDiag)を提案する。
ヒットセットの競合指向計算とfastdiagを比較し,詳細な性能解析を行う。
論文 参考訳(メタデータ) (2021-02-17T19:55:42Z) - Pass-Fail Criteria for Scenario-Based Testing of Automated Driving
Systems [0.0]
本稿では,通常運転時の自動走行システムの動作安全性を評価するための枠組みを提案する。
リスクベースのルールは、1つのテストケースからパス/フェイルを決定できない。
これは、多くの個々のテストにおける統計的パフォーマンスを考慮に入れている。
論文 参考訳(メタデータ) (2020-05-19T13:13:08Z) - Structured Prediction with Partial Labelling through the Infimum Loss [85.4940853372503]
弱い監督の目標は、収集コストの安いラベル付け形式のみを使用してモデルを学習できるようにすることである。
これは、各データポイントに対して、実際のものを含むラベルのセットとして、監督がキャストされる不完全なアノテーションの一種です。
本稿では、構造化された予測と、部分的なラベリングを扱うための無限損失の概念に基づく統一的なフレームワークを提供する。
論文 参考訳(メタデータ) (2020-03-02T13:59:41Z) - Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。
このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
論文 参考訳(メタデータ) (2019-02-02T20:09:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。