論文の概要: A SCADE Model Verification Method Based on B-Model Transformation

• arxiv url: http://arxiv.org/abs/2505.00967v1
• Date: Fri, 02 May 2025 03:05:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-05 17:21:19.887748
• Title: A SCADE Model Verification Method Based on B-Model Transformation
• Title（参考訳）: Bモデル変換に基づくSCADEモデル検証手法
• Authors: Xili Hou, Keming Wang, Huibing Zhao, Ruiyin Shi,
• Abstract要約: 本研究では,B法に基づく形式的検証フレームワークを提案する。 SCADEで直接モデリングするのが難しい抽象仕様をうまく検証します。 本研究は,アビオニクス,鉄道輸送,その他の領域における組込み制御システムに対するクロスモデル検証パラダイムを提供する。
• 参考スコア（独自算出の注目度）: 0.8437187555622164
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Due to the limitations of SCADE models in expressing and verifying abstract specifications in safety-critical systems, this study proposes a formal verification framework based on the B-Method. By establishing a semantic equivalence transformation mechanism from SCADE models to B models, a hierarchical mapping rule set is constructed, covering type systems, control flow structures, and state machines. This effectively addresses key technical challenges such as loop-equivalent transformation proof for high-order operators and modeling of temporal logic storage structures. The proposed method innovatively leverages the abstraction capabilities of B-Method in set theory and first-order logic, overcoming the constraints of native verification tools of SCADE in complex specification descriptions. It successfully verifies abstract specifications that are difficult to model directly in SCADE. Experimental results show that the transformed B models achieve a higher defect detection rate and improved verification efficiency in the ProB verification environment compared to the native verifier of SCADE, significantly enhancing the formal verification capability of safety-critical systems. This study provides a cross-model verification paradigm for embedded control systems in avionics, rail transportation, and other domains, demonstrating substantial engineering application value.
• Abstract（参考訳）: 安全クリティカルシステムにおける抽象仕様の表現・検証におけるSCADEモデルの限界から,B法に基づく形式的検証フレームワークを提案する。 SCADEモデルからBモデルへの意味等価変換機構を確立することにより、型システム、制御フロー構造、状態マシンをカバーする階層的なマッピングルールセットを構築する。 これは、高階演算子のループ等価変換証明や時間論理記憶構造のモデル化といった重要な技術的課題に効果的に対処する。 提案手法は,複雑な仕様記述におけるSCADEのネイティブ検証ツールの制約を克服し,集合論と一階述語論理におけるBメソッドの抽象化機能を革新的に活用する。 SCADEで直接モデリングするのが難しい抽象仕様をうまく検証します。 実験の結果,変換されたBモデルでは,SCADEのネイティブ検証よりも高い欠陥検出率とProB検証環境の検証効率が向上し,安全クリティカルシステムの形式検証能力が著しく向上した。 本研究では,アビオニクス,鉄道輸送,その他の領域における組込み制御系に対するクロスモデル検証のパラダイムを提供し,工学的応用価値を示す。

関連論文リスト

• Model Hemorrhage and the Robustness Limits of Large Language Models [119.46442117681147]
  大規模言語モデル(LLM)は、自然言語処理タスク全体で強力なパフォーマンスを示すが、デプロイメント用に修正された場合、大幅なパフォーマンス低下を経験する。 この現象をモデル出血(パラメータ変更とアーキテクチャ変更によるパフォーマンス低下)と定義する。
  論文  参考訳（メタデータ） (2025-03-31T10:16:03Z)
• Scoring Verifiers: Evaluating Synthetic Verification for Code and Reasoning [59.25951947621526]
  本稿では,既存の符号化ベンチマークをスコアとランキングデータセットに変換して,合成検証の有効性を評価する手法を提案する。 我々は4つの新しいベンチマーク(HE-R, HE-R+, MBPP-R, MBPP-R+)を公表し, 標準, 推論, 報酬に基づくLCMを用いて合成検証手法を解析した。 実験の結果, 推論はテストケースの生成を著しく改善し, テストケースのスケーリングによって検証精度が向上することがわかった。
  論文  参考訳（メタデータ） (2025-02-19T15:32:11Z)
• A Framework for Strategic Discovery of Credible Neural Network Surrogate Models under Uncertainty [0.0]
  本研究では,Occam Plausibility Algorithm for surrogate model (OPAL-surrogate)を提案する。 OPAL-surrogateは、予測ニューラルネットワークベースのサロゲートモデルを明らかにするための、体系的なフレームワークを提供する。 モデルの複雑さ、正確性、予測の不確実性の間のトレードオフをバランスさせる。
  論文  参考訳（メタデータ） (2024-03-13T18:45:51Z)
• OSM: Leveraging Model Checking for Observing Dynamic 1 behaviors in Aspect-Oriented Applications [0.0]
  観測ベース統計モデルチェック(OSM)フレームワークは、基本的なシステムコードから直接実行可能な形式モデルを構築するために開発された。 これにより、プリコンディションシフト中の電子健康記録システムの未収量性能が保証される。
  論文  参考訳（メタデータ） (2024-03-03T00:03:34Z)
• When to Update Your Model: Constrained Model-based Reinforcement Learning [50.74369835934703]
  モデルベースRL(MBRL)の非遅延性能保証のための新規で一般的な理論スキームを提案する。 続いて導いた境界は、モデルシフトとパフォーマンス改善の関係を明らかにします。 さらなる例では、動的に変化する探索からの学習モデルが、最終的なリターンの恩恵をもたらすことが示されている。
  論文  参考訳（メタデータ） (2022-10-15T17:57:43Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。 本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
  論文  参考訳（メタデータ） (2022-01-28T16:53:56Z)
• Lifted Model Checking for Relational MDPs [12.574454799055026]
  pCTL-REBELは、リレーショナルMDP上のpCTL特性を検証するためのリフトモデルチェック手法である。 pCTLモデル検査手法は, 無限領域であっても, リレーショナルMDPに対して決定可能であることを示す。
  論文  参考訳（メタデータ） (2021-06-22T13:12:36Z)
• Model-Based Counterfactual Synthesizer for Interpretation [40.01787107375103]
  機械学習モデルを解釈するためのモデルベース対実合成器(MCS)フレームワークを提案する。 まずモデルに基づく逆ファクト過程を分析し、条件付き生成逆数ネット(CGAN)を用いてベースシンセサイザーを構築する。 それらの希少なクエリに対する反ファクト宇宙をよりよく近似するために,MCSフレームワークのトレーニングを行うために,傘サンプリング手法を新たに採用した。
  論文  参考訳（メタデータ） (2021-06-16T17:09:57Z)
• Control as Hybrid Inference [62.997667081978825]
  本稿では、反復推論と償却推論のバランスを自然に仲介するCHIの実装について述べる。 連続的な制御ベンチマークでアルゴリズムのスケーラビリティを検証し、強力なモデルフリーおよびモデルベースラインを上回る性能を示す。
  論文  参考訳（メタデータ） (2020-07-11T19:44:09Z)

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

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