論文の概要: 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（参考訳）: 定式化テストカバレッジ基準に対する制御フローグラフのアノテート
- Authors: Sean Kauffman, Carlos Moreno, Sebastian Fischmeister,
- 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を自動的にアノテートするツールとして,アルゴリズムを実装した。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。