論文の概要: Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study (extended version)

• arxiv url: http://arxiv.org/abs/2502.19150v1
• Date: Wed, 26 Feb 2025 14:08:58 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-27 14:58:11.232709
• Title: Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study (extended version)
• Title（参考訳）: サービスとしてのPLCの形式的検証:CERN-GSI安全批判事例研究(拡張版)
• Authors: Ignacio D. Lopez-Miguel, Borja Fernández Adiego, Matias Salinas, Christine Betz,
• Abstract要約: 本稿では,PLC(Programmable logic controller)プログラムに対して,機能安全基準に準拠した形式的検証サービスを提案する。 形式的検証プロセスに対する要求の高まりに対応するために、コスト効率のよいソリューションを提供する。
• 参考スコア（独自算出の注目度）: 0.0
• License:
• Abstract: The increased technological complexity and demand for software reliability require organizations to formally design and verify their safety-critical programs to minimize systematic failures. Formal methods are recommended by functional safety standards (e.g., by IEC 61511 for the process industry and by the generic IEC 61508) and play a crucial role. Their structured approach reduces ambiguity in system requirements, facilitating early error detection. This paper introduces a formal verification service for PLC (programmable logic controller) programs compliant with functional safety standards, providing external expertise to organizations while eliminating the need for extensive internal training. It offers a cost-effective solution to meet the rising demands for formal verification processes. The approach is extended to include modeling time-dependent, know-how-protected components, enabling formal verification of real safety-critical applications. A case study shows the application of PLC formal verification as a service provided by CERN in a safety-critical installation at the GSI particle accelerator facility.
• Abstract（参考訳）: 技術的複雑さの増大とソフトウェア信頼性の要求により、組織は、組織的な失敗を最小限に抑えるために、安全クリティカルなプログラムを正式に設計し、検証する必要がある。 形式的手法は、機能的安全基準(例えば、プロセス産業のIEC 61511と一般的なIEC 61508)によって推奨され、重要な役割を果たす。 彼らの構造化されたアプローチは、システム要件の曖昧さを減らし、早期エラー検出を容易にする。 本稿では,機能安全基準に準拠したPLC(プログラマブルロジックコントローラ)プログラムの形式的検証サービスを導入し,組織に外部の専門知識を提供しながら,広範囲な内部トレーニングの必要性を排除した。 形式的検証プロセスに対する要求の高まりに対応するために、コスト効率のよいソリューションを提供する。 このアプローチは、時間に依存したノウハウ保護されたコンポーネントのモデリングを含むように拡張されており、実際の安全クリティカルなアプリケーションの正式な検証を可能にしている。 ケーススタディでは、CERNがGSI粒子加速器施設の安全クリティカルな設備に提供したサービスとしてのPLC形式検証の適用例を示した。

関連論文リスト

• Qualitative Analysis for Validating IEC 62443-4-2 Requirements in DevSecOps [0.8874671354802572]
  本稿では,ISA/IEC 62443-4-2の標準コンポーネント要件の自動検証に着目する。 私たちの分析は、現在利用可能なツールによって確立されているカバレッジを示し、完全な自動化を実現するために、現在のギャップに光を当てています。
  論文  参考訳（メタデータ） (2023-10-13T10:24:58Z)
• Klever: Verification Framework for Critical Industrial C Programs [0.0]
  我々は,大規模かつ重要な産業用Cプログラムに自動ソフトウェア検証ツールを適用する労力を削減するために,Kleverソフトウェア検証フレームワークを提案する。 既存のツールは、環境モデリング、要件の仕様、ターゲットプログラムの多くのバージョンと構成の検証、検証結果のエキスパートアセスメントなど、広く採用されている手段を提供していない。
  論文  参考訳（メタデータ） (2023-09-28T13:23:59Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)
• Rethinking Certification for Trustworthy Machine Learning-Based Applications [3.886429361348165]
  機械学習(ML)は、非決定論的振る舞いを持つ高度なアプリケーションの実装にますます使われています。 既存の認証スキームは、MLモデル上に構築された非決定論的アプリケーションにはすぐには適用されない。 本稿では、現状の認定制度の課題と欠陥を分析し、オープンな研究課題について論じ、MLベースのアプリケーションのための最初の認定制度を提案する。
  論文  参考訳（メタデータ） (2023-05-26T11:06:28Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。 次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。 これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
  論文  参考訳（メタデータ） (2022-08-23T05:02:09Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。 本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
  論文  参考訳（メタデータ） (2022-01-28T16:53:56Z)
• 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 Abstraction-based Method to Verify Multi-Agent Deep Reinforcement-Learning Behaviours [8.95294551927446]
  マルチエージェント強化学習(RL)はしばしば、学習エージェントの安全な行動を保証するために苦労する。 本稿では,形式検証と(深度)RLアルゴリズムを組み合わせることで,形式化された安全制約の満足度を保証する手法を提案する。
  論文  参考訳（メタデータ） (2021-02-02T11:12:30Z)
• Evaluating the Safety of Deep Reinforcement Learning Models using Semi-Formal Verification [81.32981236437395]
  本稿では,区間分析に基づく半形式的意思決定手法を提案する。 本手法は, 標準ベンチマークに比較して, 形式検証に対して比較結果を得る。 提案手法は, 意思決定モデルにおける安全性特性を効果的に評価することを可能にする。
  論文  参考訳（メタデータ） (2020-10-19T11:18:06Z)
• A Survey of Algorithms for Black-Box Safety Validation of Cyber-Physical Systems [30.638615396429536]
  安全クリティカルな人工知能の普及により、この研究は、CPSの最先端の安全検証技術の調査を提供する。 本稿では,最適化,経路計画,強化学習,重要サンプリングの分野におけるアルゴリズムについて論じる。 自動運転車や航空機衝突回避システムなど、安全クリティカルな応用の概要を概説する。
  論文  参考訳（メタデータ） (2020-05-06T17:31:51Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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