論文の概要: Diagnosing Violations of State-based Specifications in iCFTL
- arxiv url: http://arxiv.org/abs/2509.17776v1
- Date: Mon, 22 Sep 2025 13:40:02 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-09-30 14:24:41.880792
- Title: Diagnosing Violations of State-based Specifications in iCFTL
- Title（参考訳）: iCFTLにおける状態ベース仕様の違反診断
- Authors: Cristina Stratan, Claudio Mandrioli, Domenico Bianculli,
- Abstract要約: 本稿では,後方データフロー解析に基づく診断手法を提案する。
提案手法をプロトタイプツールであるiCFTL-Diagnosticsに実装し,10のソフトウェアプロジェクトを対象とした112の仕様で評価する。
本ツールは,112の仕様のうち100の関連文を90%の精度で識別する。
- 参考スコア（独自算出の注目度）: 1.1059590443280727
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: As modern software systems grow in complexity and operate in dynamic environments, the need for runtime analysis techniques becomes a more critical part of the verification and validation process. Runtime verification monitors the runtime system behaviour by checking whether an execution trace - a sequence of recorded events - satisfies a given specification, yielding a Boolean or quantitative verdict. However, when a specification is violated, such a verdict is often insufficient to understand why the violation happened. To fill this gap, diagnostics approaches aim to produce more informative verdicts. In this paper, we address the problem of generating informative verdicts for violated Inter-procedural Control-Flow Temporal Logic (iCFTL) specifications that express constraints over program variable values. We propose a diagnostic approach based on backward data-flow analysis to statically determine the relevant statements contributing to the specification violation. Using this analysis, we instrument the program to produce enriched execution traces. Using the enriched execution traces, we perform the runtime analysis and identify the statements whose execution led to the specification violation. We implemented our approach in a prototype tool, iCFTL-Diagnostics, and evaluated it on 112 specifications across 10 software projects. Our tool achieves 90% precision in identifying relevant statements for 100 of the 112 specifications. It reduces the number of lines that have to be inspected for diagnosing a violation by at least 90%. In terms of computational cost, iCFTL-Diagnostics generates a diagnosis within 7 min, and requires no more than 25 MB of memory. The instrumentation required to support diagnostics incurs an execution time overhead of less than 30% and a memory overhead below 20%.
- Abstract（参考訳）: 現代のソフトウェアシステムが複雑さを増し、動的環境で運用されるようになると、ランタイム分析技術の必要性が検証と検証プロセスにおいてより重要になる。
実行時の検証は、実行トレース(記録されたイベントのシーケンス)が所定の仕様を満たすかどうかをチェックして実行時のシステム動作を監視する。
しかし、仕様が違反した場合、そのような判断は、なぜ違反が起きたのかを理解するのに不十分であることが多い。
このギャップを埋めるために、診断アプローチはより情報的な評定を生み出すことを目的としている。
本稿では,プログラム変数値に対する制約を規定する命令間制御-フロー時相論理(iCFTL)仕様に違反する情報的検証を生成する問題に対処する。
本稿では,後方データフロー解析に基づく診断手法を提案し,仕様違反の原因となる文を静的に判定する。
この分析により,プログラムはリッチな実行トレースを生成する。
リッチな実行トレースを使用してランタイム分析を行い、実行が仕様違反に繋がったステートメントを特定します。
提案手法をプロトタイプツールであるiCFTL-Diagnosticsに実装し,10のソフトウェアプロジェクトを対象とした112の仕様で評価した。
本ツールは,112の仕様のうち100の関連文を90%の精度で識別する。
違反を診断するために検査しなければならない線数を、少なくとも90%削減する。
計算コストの面では、iCFTL-Diagnosticsは7分以内に診断を生成し、25MB以上のメモリを必要とする。
診断をサポートするために必要な機器は、実行時のオーバーヘッドが30%未満で、メモリオーバーヘッドが20%未満である。
関連論文リスト
- Efficient Conformance Checking of Rich Data-Aware Declare Specifications (Extended) [49.46686813437884]
一般的なデータ型やデータ条件とリッチな設定で,データを考慮した最適アライメントを計算可能であることを示す。
これは、制御フローとデータ依存関係を扱うために、よく知られた2つのアプローチを慎重に組み合わせることで達成される。
論文 参考訳（メタデータ） (2025-06-30T10:16:21Z) - Computation Tree Logic Guided Program Repair [10.880298593486671]
本稿では,CTL特性によって誘導される無限状態プログラムの自動修復機構を提案する。
我々のフレームワークは,プログラムとCTLプロパティをDatalogのファクトとルールにエンコードし,解析ルールをパスするために事実を変更することで修復を行う。
提案手法は,小規模ベンチマークでは56.6%,実世界のベンチマークでは88.5%であり,ベースライン性能は27.7%,76.9%であった。
論文 参考訳（メタデータ） (2025-02-21T09:59:38Z) - Search-based Trace Diagnostic [7.771496745635823]
実行トレースが要件に違反している場合、エンジニアは違反の原因を理解する必要がある。
本稿では,CPS要求に対する新しいトレース診断手法であるサーチベーストレース診断(SBTD)を提案する。
論文 参考訳（メタデータ） (2024-06-25T04:24:21Z) - Defining and executing temporal constraints for evaluating engineering
artifact compliance [56.08728135126139]
プロセスコンプライアンスは、実際のエンジニアリング作業が記述されたエンジニアリングプロセスに可能な限り密接に従うことを保証することに焦点を当てます。
これらのプロセスの制約をチェックすることは、依然として大変な作業であり、多くの手作業を必要とし、プロセスの後半にエンジニアにフィードバックを提供する。
関連するエンジニアリングアーティファクト間の時間的制約を,アーティファクトの変更毎に段階的にチェックする,自動制約チェックアプローチを提案する。
論文 参考訳（メタデータ） (2023-12-20T13:26:31Z) - FastDiagP: An Algorithm for Parallelized Direct Diagnosis [64.65251961564606]
FastDiagは、競合を事前に決定せずに診断計算をサポートする典型的な直接診断アルゴリズムである。
本稿では,投機的プログラミングのアイデアに基づく新しいアルゴリズムであるFastDiagPを提案する。
このメカニズムは、高速な回答で一貫性チェックを提供し、アルゴリズムのランタイムパフォーマンスを高めるのに役立つ。
論文 参考訳（メタデータ） (2023-05-11T16:26:23Z) - Measuring Rule-based LTLf Process Specifications: A Probabilistic
Data-driven Approach [2.5407767658470726]
宣言的プロセス仕様は、有限トレース上の線形時間論理に基づくルールによってプロセスの振舞いを定義します。
マイニングの文脈では、これらの仕様は情報システムによって記録された複数セットの実行から推論され、チェックされる。
本稿では,イベントログに対する仕様書の満足度を測定する手法を提案する。
論文 参考訳（メタデータ） (2023-05-09T13:07:01Z) - PULL: Reactive Log Anomaly Detection Based On Iterative PU Learning [58.85063149619348]
本稿では,推定故障時間ウィンドウに基づくリアクティブ異常検出のための反復ログ解析手法PULLを提案する。
我々の評価では、PULLは3つの異なるデータセットで10のベンチマークベースラインを一貫して上回っている。
論文 参考訳（メタデータ） (2023-01-25T16:34:43Z) - Execution Time Program Verification With Tight Bounds [6.36836017515443]
本稿では,コア命令型プログラミング言語の実行時間境界を推論するための証明システムを提案する。
3つのケースに対してHoareロジックを定義し、注釈付きコスト対応操作セマンティクスに関してその健全性を証明する。
証明システムの実用性は、サンプルプログラムに適用するために必要な異なるモジュールのOCamlの実装で実証される。
論文 参考訳（メタデータ） (2022-10-20T09:02:13Z) - Anytime Diagnosis for Reconfiguration [52.77024349608834]
我々は、いつでも直接診断できるflexdiagを紹介し分析する。
特徴モデルの領域からの構成ベンチマークと自動車領域からの産業構成知識ベースを使用して、性能および診断品質に関するアルゴリズムを評価します。
論文 参考訳（メタデータ） (2021-02-19T11:45:52Z) - An Efficient Diagnosis Algorithm for Inconsistent Constraint Sets [68.8204255655161]
過制約問題における最小限の障害制約を識別する分割・分散型診断アルゴリズム(FastDiag)を提案する。
ヒットセットの競合指向計算とfastdiagを比較し,詳細な性能解析を行う。
論文 参考訳（メタデータ） (2021-02-17T19:55:42Z) - Feature Engineering for Scalable Application-Level Post-Silicon
Debugging [0.456877715768796]
シリコン後のシステム・オン・チップ(SoCs)検証における可観測性向上と根本原因診断の両方法を提案する。
メッセージ選択のための典型的なアプリケーションにおける対話フローの仕様をモデル化する。
我々は、診断問題を、バグのトレースを外れ値として、バグのないトレースを異常値/正常値として識別するものとして定義する。
論文 参考訳（メタデータ） (2021-02-08T22:11:59Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。