論文の概要: KBX: Verified Model Synchronization via Formal Bidirectional Transformation
- arxiv url: http://arxiv.org/abs/2404.18771v2
- Date: Wed, 1 May 2024 15:08:32 GMT
- ステータス: 処理完了
- システム内更新日: 2024-05-02 10:59:25.983494
- 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 % 削減されたことを示す。
関連論文リスト
- Binarized Diffusion Model for Image Super-Resolution [61.963833405167875]
画像SRのための新しいバイナライズ拡散モデルBI-DiffSRを提案する。
モデル構造では、二項化に最適化されたUNetアーキテクチャを設計する。
我々は,一貫した次元を維持するために,一貫した画素ダウンサンプル (CP-Down) と一貫したピクセルアップサンプル (CP-Up) を提案する。
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) - CARE: Coherent Actionable Recourse based on Sound Counterfactual
Explanations [0.0]
本稿では,モデルおよびユーザレベルのデシダータに対処するモジュール型説明フレームワークであるCAREを紹介する。
モデルに依存しないアプローチとして、CAREはブラックボックスモデルに対して複数の多様な説明を生成する。
論文 参考訳(メタデータ) (2021-08-18T15:26:59Z) - Equivalence of Segmental and Neural Transducer Modeling: A Proof of
Concept [56.46135010588918]
RNN-Transducerモデルとセグメントモデル(直接HMM)の広く使われているクラスが等価であることを証明する。
空白確率はセグメント長確率に変換され,その逆も示された。
論文 参考訳(メタデータ) (2021-04-13T11:20:48Z) - On Exploiting Hitting Sets for Model Reconciliation [53.81101846598925]
ヒューマン・アウェア・プランニングにおいて、プランニング・エージェントは、その計画がなぜ最適なのかを人間に説明する必要があるかもしれない。
この手法はモデル和解と呼ばれ、エージェントはモデルと人間のモデルの違いを調和させようとする。
我々は,計画の領域を超えて拡張されたモデル和解のための論理ベースのフレームワークを提案する。
論文 参考訳(メタデータ) (2020-12-16T21:25:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。