論文の概要: SafeDSE: Joint Exploration of Safety Architecture Patterns, Mapping, and Scheduling for Dataflow Applications With Safety Arguments (Extended Version)

• arxiv url: http://arxiv.org/abs/2610.16213v1
• Date: Mon, 12 Oct 2026 05:43:56 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-15 21:06:15.313991
• Title: SafeDSE: Joint Exploration of Safety Architecture Patterns, Mapping, and Scheduling for Dataflow Applications With Safety Arguments (Extended Version)
• Title（参考訳）: SafeDSE: 安全条件付きデータフローアプリケーションのための安全アーキテクチャパターン、マッピング、スケジューリングの共同探索(拡張バージョン)
• Abstract要約: 本報告では,同期データフローアプリケーションのための設計空間探索フレームワークであるSafeDSEについて述べる。 1つの宣言的制約モデルが各アクターのパターン、障害モデルに必要な配置、静的順序スケジュール、プラットフォームを決定する。 独立検証器はすべてのソリューションを再チェックし、ジェネレータはそのチェックを安全引数の証拠にします。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Embedded platforms increasingly host safety-related streaming functions next to less critical ones. Whether a safety architecture pattern, such as a doer/checker pair, protects a function depends on the cores that run its components. Their schedule must meet the throughput requirement, and mixing safety integrity levels (SILs) on one core raises development cost. This report presents SafeDSE, a design space exploration framework for synchronous dataflow applications. One declarative constraint model decides the pattern of each actor, the placement that the fault model requires, the static-order schedule, and the platform, and prices SIL promotion. Guards activate the chosen patterns in a fixed graph that holds all of them, and node potentials encode throughput. An independent verifier re-checks every solution, and a generator turns its checks into evidence of a safety argument in Goal Structuring Notation. On 9 benchmark instances under period bounds, no rule that fixes patterns before mapping was both always feasible and never more expensive under conservative pricing, while joint exploration was. In the generated arguments, 49 to 62% of the leaves cite verifier checks; the rest are claims a mapping cannot discharge. Optimality within the model was proven for all synthetic graphs with up to 16 actors. This extended version adds the full model, the verifier and generator in detail, the complete catalog and parameters, and a proof of the potential characterization. It also reports every experiment per instance, a mutation analysis of the verifier, and the negative results of the development.
• Abstract（参考訳）: 組込みプラットフォームは、あまり重要でないものの横にある安全関連ストリーミング機能をますますホストしている。 ドア/チェッカーペアのような安全アーキテクチャパターンが関数を保護するかどうかは、そのコンポーネントを実行するコアに依存する。 彼らのスケジュールはスループット要件を満たす必要があり、一方のコアに安全整合性レベル(SIL)を混合することで、開発コストが上昇する。 本報告では,同期データフローアプリケーションのための設計空間探索フレームワークであるSafeDSEについて述べる。 1つの宣言的制約モデルは、各アクターのパターン、障害モデルに必要な配置、静的順序スケジュール、プラットフォームを決定し、SILプロモーションを値付けする。 ガードは、すべてのグラフを保持する固定グラフで選択されたパターンを起動し、ノード電位はスループットを符号化する。 独立検証器はすべての解を再チェックし、生成器はそのチェックをゴール構造化表記法(Goal Structuring Notation)の安全性議論の証拠にします。 期間境界下の9つのベンチマークインスタンスでは、マッピング前のパターンを修正するルールは常に実現可能で、保守的な価格の下では高価ではない。 生成された議論では、葉の49～62%が検証者チェックを引用し、残りはマッピングが排出できないと主張する。 モデル内の最適性は、最大16人のアクターを持つすべての合成グラフに対して証明された。 この拡張バージョンでは、完全なモデル、検証器とジェネレータの詳細、完全なカタログとパラメータ、潜在的な特徴の証明が追加されている。 また、インスタンス毎の実験、検証者の突然変異解析、および開発におけるネガティブな結果も報告している。

関連論文リスト

• Assurance Envelopes for Autonomous Coding Agents: Minimum-Cost Evidence for Software Change [0.0]
  利用可能な証拠の少なくともコストの低いサブセットが要求された資産を再確立するかどうかを問う。 私たちは、クロージャを信頼するのではなく、クロージャによってすべての選択を検証する。 Rust、IronBlocks、Pongの結果の小さなグラフは、最小エンベロープがタスクに依存することを示している。
  論文  参考訳（メタデータ） (2026-09-14T20:06:46Z)
• What to Test Next: Interpretable Coverage Gap Discovery in Driving VLMs [52.50210189669399]
  視覚言語モデル(VLM)を駆動するには,操作設計領域(ODD)が定義する様々な条件のシーンを正確に理解する必要がある SliceScorerは、欠落したスライス推薦のための決定論的スコアリングルールである。 SliceNavは, 従来のスライス発見法よりも, 高リスクカバレッジギャップを効果的に表面化することを示す。
  論文  参考訳（メタデータ） (2026-06-01T03:18:01Z)
• ClawArena: Benchmarking AI Agents in Evolving Information Environments [61.664633997138004]
  ClawArenaは、進化する情報環境におけるAIエージェントの評価のためのベンチマークである。 それぞれのシナリオは、エージェントをノイズ、部分的、時には矛盾するトレースだけに露呈しながら、完全に隠された地上の真実を維持します。 評価は、マルチソースコンフリクト推論、動的信念修正、暗黙のパーソナライゼーションという3つの複合的な課題に基づいて構成される。
  論文  参考訳（メタデータ） (2026-04-05T17:55:23Z)
• Agentproof: Static Verification of Agent Workflow Graphs [0.0]
  エージェントフレームワークは、ツール使用の振る舞いを明示的なワークフローグラフとしてエンコードする傾向にある。 本稿では,4つの主要なエージェントフレームワークから統合抽象グラフモデルを自動的に抽出するAgentproofを提案する。 汎用的なモデルチェッカーとは異なり、Agentproofは手動モデリングを必要としない。
  論文  参考訳（メタデータ） (2026-03-20T13:56:20Z)
• Safety Under Scaffolding: How Evaluation Conditions Shape Measured Safety [0.0]
  我々は,足場が安全に与える影響について,最も制御された研究の1つを報告した。 マップ・リデュース・足場は、測定された安全性を低下させる。 同一項目における複数選択からオープンエンドフォーマットへの切り替えは、安全性スコアを5～20ポイントシフトさせる。
  論文  参考訳（メタデータ） (2026-03-08T01:37:45Z)
• SecCodeBench-V2 Technical Report [43.10947096543533]
  SecCodeBench-V2は,セキュアなコードを生成するLarge Language Model (LLM)コピロの能力を評価するためのベンチマークである。 SecCodeBench-V2は、アリババグループの工業生産から派生した98世代および修正シナリオを含む。 各シナリオに対して、SecCodeBench-V2は、機能検証とセキュリティ検証の両方に対して実行可能な概念実証(PoC)テストケースを提供する。
  論文  参考訳（メタデータ） (2026-02-17T10:47:06Z)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。 このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
  論文  参考訳（メタデータ） (2026-02-10T06:58:26Z)
• interwhen: A Generalizable Framework for Verifiable Reasoning with Test-time Monitors [47.363850513075356]
  実験時間検証フレームワークであるInterwhenを提案し, 与えられた検証結果に対して, 推論モデルの出力が有効であることを保証する。 検証された推論は、物理的な世界にエージェントを配置するといった高度なシナリオにおいて重要な目標である。
  論文  参考訳（メタデータ） (2026-02-05T08:35:01Z)
• Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
  本稿では,dLLMの復号化機構をモデル属性の強力なツールとして利用できることを示す。 本稿では、デコードステップ間の構造的関係を捉え、モデル固有の振る舞いをよりよく明らかにする、DDM(Directed Decoding Map)と呼ばれる新しい情報抽出手法を提案する。
  論文  参考訳（メタデータ） (2025-10-02T06:25:10Z)

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

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