論文の概要: Formal Verification of Digital Twins with TLA and Information Leakage Control
- arxiv url: http://arxiv.org/abs/2411.18798v1
- Date: Wed, 27 Nov 2024 22:52:36 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-12-02 15:18:10.762245
- Title: Formal Verification of Digital Twins with TLA and Information Leakage Control
- Title（参考訳）: TLAと情報漏洩制御を用いたディジタル双生児の形式的検証
- Authors: Luwen Huang, Lav R. Varshney, Karen E. Willcox,
- Abstract要約: デジタルツイン検証は、仮想表現、物理的環境、および物理と仮想の間の情報の双方向の流れの不確実性のために困難である。
本稿では,不確実なプロセスを形式的に検証可能な有限状態機械に変換することによって,ディジタル双対動作の特定と検証を行う手法を提案する。
本研究では,無人航空機のディジタル双対に対して,物理的・仮想的・仮想的データフローの同期を検証し,意図しない誤認識を検出する。
- 参考スコア（独自算出の注目度）: 15.387256204743407
- License:
- Abstract: Verifying the correctness of a digital twin provides a formal guarantee that the digital twin operates as intended. Digital twin verification is challenging due to the presence of uncertainties in the virtual representation, the physical environment, and the bidirectional flow of information between physical and virtual. A further challenge is that a digital twin of a complex system is composed of distributed components. This paper presents a methodology to specify and verify digital twin behavior, translating uncertain processes into a formally verifiable finite state machine. We use the Temporal Logic of Actions (TLA) to create a specification, an implementation abstraction that defines the properties required for correct system behavior. Our approach includes a novel weakening of formal security properties, allowing controlled information leakage while preserving theoretical guarantees. We demonstrate this approach on a digital twin of an unmanned aerial vehicle, verifying synchronization of physical-to-virtual and virtual-to-digital data flows to detect unintended misalignments.
- Abstract（参考訳）: デジタルツインの正しさを検証することは、デジタルツインが意図した通りに動作するという正式な保証を提供する。
デジタルツイン検証は、仮想表現、物理的環境、および物理と仮想の間の情報の双方向の流れに不確実性が存在するため、困難である。
さらに難しいのは、複雑なシステムのデジタルツインが分散コンポーネントで構成されていることだ。
本稿では,不確実なプロセスを形式的に検証可能な有限状態機械に変換することによって,ディジタル双対動作の特定と検証を行う手法を提案する。
我々は、TLA(Temporal Logic of Actions)を使用して、正しいシステム動作に必要なプロパティを定義する実装抽象化である仕様を作成します。
弊社のアプローチは、公式なセキュリティ特性の新たな弱体化を含み、理論的保証を維持しつつ、制御された情報漏洩を可能にする。
本研究では,無人航空機のディジタル双対に対して,物理的・仮想的・仮想的データフローの同期を検証し,意図しない誤認識を検出する。
関連論文リスト
- Know Where You're Uncertain When Planning with Multimodal Foundation Models: A Formal Framework [54.40508478482667]
認識と計画生成の不確実性を解消し、定量化し、緩和する包括的枠組みを提案する。
本稿では,知覚と意思決定の独特な性質に合わせた手法を提案する。
この不確実性分散フレームワークは, 変動率を最大40%削減し, タスク成功率をベースラインに比べて5%向上させることを示した。
論文 参考訳（メタデータ） (2024-11-03T17:32:00Z) - Med-Real2Sim: Non-Invasive Medical Digital Twins using Physics-Informed Self-Supervised Learning [15.106435744696013]
デジタルツイン(Digital twin)は、数学的モデリングを用いてその定義する特徴を特徴づけ、シミュレートする現実世界の物理現象の仮想レプリカである。
非侵襲的な患者健康データのみを用いてデジタル双対モデルパラメータを同定する手法を提案する。
論文 参考訳（メタデータ） (2024-02-29T23:04:42Z) - From Digital Twins to Digital Twin Prototypes: Concepts, Formalization,
and Applications [55.57032418885258]
デジタル双対とは何かという合意的な定義は存在しない。
我々のデジタルツインプロトタイプ(DTP)アプローチは、組み込みソフトウェアシステムの開発と自動テストにおいて、エンジニアを支援します。
論文 参考訳（メタデータ） (2024-01-15T22:13:48Z) - Object-Centric Conformance Alignments with Synchronization (Extended Version) [57.76661079749309]
対象中心のペトリネットが一対多の関係を捉える能力と,その同一性に基づいたオブジェクトの比較と同期を行う識別子を持つペトリネットの能力を組み合わせた,新たな形式主義を提案する。
我々は、満足度変調理論(SMT)の符号化に基づく、そのようなネットに対する適合性チェック手法を提案する。
論文 参考訳（メタデータ） (2023-12-13T21:53:32Z) - Probabilistic machine learning based predictive and interpretable
digital twin for dynamical systems [0.0]
ディジタルツインを更新するための2つのアプローチが提案されている。
どちらの場合も、更新されたデジタル双生児の表現は同一である。
提案手法は、ディジタル双対モデルにおける摂動の正確な説明を提供する。
論文 参考訳（メタデータ） (2022-12-19T04:25:59Z) - The Executable Digital Twin: merging the digital and the physics worlds [0.0]
モデル順序の低減、リアルタイムモデル、状態推定、共シミュレーションなどの重要なビルディングブロックをレビューする。
これには、仮想センシング、ハイブリッドテスト、ハードウェア・イン・ザ・ループ、モデルベースの制御、モデルベースの診断が含まれる。
論文 参考訳（メタデータ） (2022-10-25T08:35:08Z) - Knowledge Equivalence in Digital Twins of Intelligent Systems [3.7953718547499045]
本論文は,知的システムのデジタル双対モデルに焦点をあてる。
このようなインテリジェントな物理システムのモデリングには、仮想空間における知識認識能力を複製する必要がある。
本稿では,知識比較と更新による知識等価性の概念と等価性維持手法を提案する。
論文 参考訳（メタデータ） (2022-04-15T14:31:17Z) - Automatic digital twin data model generation of building energy systems
from piping and instrumentation diagrams [58.720142291102135]
建物からP&IDのシンボルや接続を自動で認識する手法を提案する。
シンボル認識,線認識,およびデータセットへの接続の導出にアルゴリズムを適用する。
このアプローチは、制御生成、(分散)モデル予測制御、障害検出といった、さらなるプロセスで使用することができる。
論文 参考訳（メタデータ） (2021-08-31T15:09:39Z) - gradSim: Differentiable simulation for system identification and
visuomotor control [66.37288629125996]
本稿では,微分可能マルチフィジカルシミュレーションと微分可能レンダリングを活用し,3次元監督への依存を克服するフレームワークであるgradsimを提案する。
当社の統合グラフは、状態ベースの(3D)監督に頼ることなく、挑戦的なバイスモメータ制御タスクで学習を可能にします。
論文 参考訳（メタデータ） (2021-04-06T16:32:01Z) - A Probabilistic Graphical Model Foundation for Enabling Predictive
Digital Twins at Scale [0.0]
結合ダイナミクスシステムの集合として、アセットツインシステムの抽象化を作成します。
本研究では,無人航空機のディジタル双対構造を実現するために,モデルがどのようにインスタンス化されるかを実証する。
論文 参考訳（メタデータ） (2020-12-10T17:33:59Z) - Digital Twins: State of the Art Theory and Practice, Challenges, and
Open Research Questions [62.67593386796497]
この研究は、様々なDT機能と現在のアプローチ、デジタルツインの実装と導入の遅れの背景にある欠点と理由を探求する。
この遅延の主な理由は、普遍的な参照フレームワークの欠如、ドメイン依存、共有データのセキュリティ上の懸念、デジタルツインの他の技術への依存、定量的メトリクスの欠如である。
論文 参考訳（メタデータ） (2020-11-02T19:08:49Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。