論文の概要: KBX: Verified Model Synchronization via Formal Bidirectional Transformation
- arxiv url: http://arxiv.org/abs/2404.18771v1
- Date: Mon, 29 Apr 2024 15:05:27 GMT
- ステータス: 処理完了
- システム内更新日: 2024-04-30 13:18:30.911485
- Title: KBX: Verified Model Synchronization via Formal Bidirectional Transformation
- Title（参考訳）: KBX:形式的双方向変換による検証モデル同期
- Authors: Jianhong Zhao, Yongwang Zhao, Peisen Yao, Fanlang Zeng, Bohua Zhan, Kui Ren,
- Abstract要約: 双方向変換(BX)は、これらのモデルを自動的に同期するアプローチである。
既存のBXフレームワークには、これらのモデルの一貫性を厳格に強制するための正式な検証がない。
本稿では,検証モデル同期のための形式変換フレームワークKBXを紹介する。
- 参考スコア（独自算出の注目度）: 10.119816058971539
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Complex safety-critical systems require multiple models for a comprehensive description, resulting in error-prone development and laborious verification. Bidirectional transformation (BX) is an approach to automatically synchronizing these models. However, existing BX frameworks lack formal verification to enforce these models' consistency rigorously. This paper introduces KBX, a formal bidirectional transformation framework for verified model synchronization. First, we present a matching logic-based BX model, providing a logical foundation for constructing BX definitions within the $\mathbb{K}$ framework. Second, we propose algorithms to synthesize formal BX definitions from unidirectional ones, which allows developers to focus on crafting the unidirectional definitions while disregarding the reverse direction and missing information recovery for synchronization. Afterward, we harness $\mathbb{K}$ to generate a formal synchronizer from the synthesized definitions for consistency maintenance and verification. To evaluate the effectiveness of KBX, we conduct a comparative analysis against existing BX frameworks. Furthermore, we demonstrate the application of KBX in constructing a BX between UML and HCSP for real-world scenarios, showcasing an 82.8\% reduction in BX development effort compared to manual specification writing in $\mathbb{K}$.
- Abstract（参考訳）: 複雑な安全クリティカルなシステムは包括的記述のために複数のモデルを必要とするため、エラーが発生しやすい開発と厳密な検証が生じる。
双方向変換(BX)は、これらのモデルを自動的に同期するアプローチである。
しかし、既存のBXフレームワークはこれらのモデルの一貫性を厳格に強制する正式な検証を欠いている。
本稿では,検証モデル同期のための形式的双方向変換フレームワークKBXを紹介する。
まず、マッチング論理に基づくBXモデルを示し、$\mathbb{K}$フレームワーク内でBX定義を構築するための論理的基盤を提供する。
第2に,一方向定義から形式的BX定義を合成するアルゴリズムを提案する。
その後、$\mathbb{K}$を使用して、一貫性の維持と検証のために合成された定義から形式的シンクロナイザを生成する。
KBXの有効性を評価するため,既存のBXフレームワークとの比較分析を行った。
さらに,UML と HCSP 間の BX 構築における KBX の応用を実世界のシナリオに適用し,$\mathbb{K}$ のマニュアル仕様記述に比べて BX 開発作業が82.8 % 削減されたことを示す。
関連論文リスト
- COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
反復改良は、複雑なタスクにおける大規模言語モデル(LLM)の能力を高める効果的なパラダイムとして登場した。
我々はこれらの課題を克服するために、コンテキストワイズ順序非依存言語モデリング(COrAL)を提案する。
当社のアプローチでは、管理可能なコンテキストウィンドウ内で複数のトークン依存関係をモデル化しています。
論文 参考訳（メタデータ） (2024-10-12T23:56:19Z) - Backward Compatibility in Attributive Explanation and Enhanced Model Training Method [0.0]
本稿では,事前および更新後のモデル間の特徴属性説明の後方互換性を評価する指標であるBCXを紹介する。
BCXは、事前および更新後のモデルの説明の間の平均合意を計算するために、実践的な合意メトリクスを利用する。
モデルの説明の中でL2距離を利用して,すべての合意基準を改善するBCXRの普遍的変種を提案する。
論文 参考訳（メタデータ） (2024-08-05T08:14:32Z) - Binarized Diffusion Model for Image Super-Resolution [61.963833405167875]
超圧縮アルゴリズムであるバイナリ化は、高度な拡散モデル(DM)を効果的に加速する可能性を提供する
既存の二項化法では性能が著しく低下する。
画像SRのための新しいバイナライズ拡散モデルBI-DiffSRを提案する。
論文 参考訳（メタデータ） (2024-06-09T10:30:25Z) - Recurrent Complex-Weighted Autoencoders for Unsupervised Object Discovery [62.43562856605473]
複雑な重み付き再帰的アーキテクチャの計算上の優位性について論じる。
本稿では,反復的制約満足度を実現する完全畳み込みオートエンコーダSynCxを提案する。
論文 参考訳（メタデータ） (2024-05-27T15:47:03Z) - A Novel Decision Ensemble Framework: Customized Attention-BiLSTM and
XGBoost for Speculative Stock Price Forecasting [2.011511123338945]
本稿では、投機的株式Bitcoin-USD(BTC-USD)の日替価格を予測するための新しいフレームワーク、CAB-XDEを提案する。
CAB-XDEフレームワークは、カスタマイズされた双方向長短期メモリ(BiLSTM)とアテンション機構とXGBoostアルゴリズムを統合している。
提案されたCAB-XDEフレームワークは、Yahoo Financeから供給された不安定なBitcoin市場で実証的に検証されている。
論文 参考訳（メタデータ） (2024-01-05T17:13:30Z) - Bidirectional Trained Tree-Structured Decoder for Handwritten
Mathematical Expression Recognition [51.66383337087724]
Handwriting Mathematical Expression Recognition (HMER) タスクは、OCRの分野における重要な分岐である。
近年の研究では、双方向コンテキスト情報の導入により、HMERモデルの性能が大幅に向上することが示されている。
本稿では,MF-SLT と双方向非同期トレーニング (BAT) 構造を提案する。
論文 参考訳（メタデータ） (2023-12-31T09:24:21Z) - OCTAL: Graph Representation Learning for LTL Model Checking [5.22145960878624]
GRLベースの新しいフレームワークモデルは、グラフ構造化システムと仕様の表現を学習するために設計されている。
実験により、モデルが有望な精度を達成し、標準SOTAモデルチェッカーに対する全体的なスピードアップが最大で11倍になることが示された。
論文 参考訳（メタデータ） (2023-08-19T15:11:18Z) - The Bayesian Context Trees State Space Model for time series modelling
and forecasting [8.37609145576126]
実数値時系列に対してリッチな混合モデルを開発するための階層的ベイズフレームワークが導入された。
最上位では、有意義な離散状態が、最新のサンプルの適切な定量値として特定される。
下位レベルでは、実数値時系列(ベースモデル)の異なる任意のモデルが各状態と関連付けられている。
論文 参考訳（メタデータ） (2023-08-02T02:40:42Z) - BB-GCN: A Bi-modal Bridged Graph Convolutional Network for Multi-label
Chest X-Ray Recognition [7.110986667249555]
マルチラベル胸部X線(英語版)(CXR)認識は、異なる病理の複数のラベルを同時に診断し識別する。
従来の手法は、ローカルラベル情報をモデル化するために、状態変数の符号化とアテンションメカニズムに頼っていた。
Bi-modal Bridged Graph Convolutional Network (BB-GCN) モデルを提案する。
論文 参考訳（メタデータ） (2023-02-22T01:03:53Z) - Error-based Knockoffs Inference for Controlled Feature Selection [49.99321384855201]
本手法では, ノックオフ特徴量, エラーベース特徴重要度統計量, ステップダウン手順を一体化して, エラーベースのノックオフ推定手法を提案する。
提案手法では回帰モデルを指定する必要はなく,理論的保証で特徴選択を処理できる。
論文 参考訳（メタデータ） (2022-03-09T01:55:59Z) - On Exploiting Hitting Sets for Model Reconciliation [53.81101846598925]
ヒューマン・アウェア・プランニングにおいて、プランニング・エージェントは、その計画がなぜ最適なのかを人間に説明する必要があるかもしれない。
この手法はモデル和解と呼ばれ、エージェントはモデルと人間のモデルの違いを調和させようとする。
我々は,計画の領域を超えて拡張されたモデル和解のための論理ベースのフレームワークを提案する。
論文 参考訳（メタデータ） (2020-12-16T21:25:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。