論文の概要: OSM: Leveraging Model Checking for Observing Dynamic 1 behaviors in
Aspect-Oriented Applications
- arxiv url: http://arxiv.org/abs/2403.01349v1
- Date: Sun, 3 Mar 2024 00:03:34 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-05 14:10:48.669445
- Title: OSM: Leveraging Model Checking for Observing Dynamic 1 behaviors in
Aspect-Oriented Applications
- Title（参考訳）: OSM:アスペクト指向アプリケーションにおける動的1動作監視のためのモデルチェックの活用
- Authors: Anas AlSobeh
- Abstract要約: 観測ベース統計モデルチェック(OSM)フレームワークは、基本的なシステムコードから直接実行可能な形式モデルを構築するために開発された。
これにより、プリコンディションシフト中の電子健康記録システムの未収量性能が保証される。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In the intricate domain of software systems verification, dynamically model
checking multifaceted system characteristics remains paramount, yet
challenging. This research proposes the advanced observe-based statistical
model-checking (OSM) framework, devised to craft executable formal models
directly from foundational system code. Leveraging model checking predicates,
the framework melds seamlessly with aspect-oriented programming paradigms,
yielding a potent method for the analytical verification of varied behavioral
attributes. Exploiting the transformative capacity of OSM framework, primary
system code undergoes a systematic metamorphosis into multifaceted analysis
constructs. This not only simplifies the model verification process but also
orchestrates feature interactions using an innovative observing join point
abstraction mechanism. Within this framework, components encompassing parsing,
formal verification, computational analytics, and rigorous validation are
intrinsically interwoven. Marrying the principles of model checking with
aspect-oriented (AO) modularization, OSM framework stands as a paragon,
proficiently scrutinizing and affirming system specifications. This ensures the
unyielding performance of electronic health record systems amidst shifting
preconditions. OSM framework offers runtime verification of both
object-oriented and AO deployments, positioning itself as an indispensable
open-source resource, poised to automate the enhancement of system performance
and scalability.
- Abstract（参考訳）: 複雑なソフトウェアシステム検証の領域では、動的モデルチェックによる多面システム特性の検証が依然として最重要でありながら困難である。
本研究は,基本システムコードから直接実行可能な形式モデルを構築するために考案された,高度な観測ベース統計モデルチェック(OSM)フレームワークを提案する。
モデルチェックの述語を活用することで、フレームワークはアスペクト指向のプログラミングパラダイムとシームレスに融合し、さまざまな行動属性の分析的検証のための強力な方法をもたらす。
OSMフレームワークの変換能力の爆発により、一次システムは多面解析構造への体系的変態を行う。
これはモデル検証プロセスを単純化するだけでなく、革新的な観察ジョインポイント抽象化メカニズムを使って機能インタラクションをオーケストレーションする。
このフレームワーク内では、解析、形式検証、計算分析、厳密な検証を含むコンポーネントが本質的に織り込まれている。
アスペクト指向(AO)モジュール化によるモデルチェックの原則を反映して、OSMフレームワークはパラゴンであり、十分に精査し、システム仕様を確認します。
これにより、プレコンディションシフト中の電子健康記録システムの未収量性能が保証される。
OSMフレームワークは、オブジェクト指向とAOの両方のデプロイメントのランタイム検証を提供し、システムパフォーマンスとスケーラビリティの強化を自動化するために、自分自身を必須のオープンソースリソースとして位置づける。
関連論文リスト
- Process Modeling With Large Language Models [45.129578769739]
本稿では,大規模言語モデル(LLM)のプロセスモデリングへの統合について検討する。
プロセスモデルの自動生成と反復的改善にLLMを利用するフレームワークを提案する。
予備的な結果は、プロセスモデリングタスクを合理化するフレームワークの能力を示している。
論文 参考訳（メタデータ） (2024-03-12T11:27:47Z) - A Unified Framework for Probabilistic Verification of AI Systems via
Weighted Model Integration [13.275592130089953]
AIシステムの確率形式検証(PFV)はその初期段階にある。
Weighted Model Integration (WMI)に基づくAIシステムのPFV統合フレームワークを提案する。
この削減により、幅広い機械学習モデルに対して、公正性、ロバスト性、モノトニック性など、多くの興味のある性質の検証が可能になる。
論文 参考訳（メタデータ） (2024-02-07T14:24:04Z) - White-box validation of quantitative product lines by statistical model
checking and process mining [1.0918484507642576]
本稿では,統計的モデル検査 (SMC) とプロセスマイニング (PM) を統合することで,ソフトウェア製品ライン (PL) モデルの検証手法を提案する。
提案手法は,PL工学領域における機能指向言語QFLanに着目し,豊富なクロスツリーと量的制約を持つPLのモデリングを可能にする。
論文 参考訳（メタデータ） (2024-01-23T17:27:13Z) - Variable Importance Matching for Causal Inference [73.25504313552516]
これらの目標を達成するためのModel-to-Matchと呼ばれる一般的なフレームワークについて説明する。
Model-to-Matchは、距離メートル法を構築するために変数重要度測定を使用する。
LASSO を用いて Model-to-Match フレームワークを運用する。
論文 参考訳（メタデータ） (2023-02-23T00:43:03Z) - When to Update Your Model: Constrained Model-based Reinforcement
Learning [50.74369835934703]
モデルベースRL(MBRL)の非遅延性能保証のための新規で一般的な理論スキームを提案する。
続いて導いた境界は、モデルシフトとパフォーマンス改善の関係を明らかにします。
さらなる例では、動的に変化する探索からの学習モデルが、最終的なリターンの恩恵をもたらすことが示されている。
論文 参考訳（メタデータ） (2022-10-15T17:57:43Z) - Relational Action Bases: Formalization, Effective Safety Verification,
and Invariants (Extended Version) [67.99023219822564]
我々はリレーショナルアクションベース(RAB)の一般的な枠組みを紹介する。
RABは両方の制限を解除することで既存のモデルを一般化する。
データ対応ビジネスプロセスのベンチマークにおいて、このアプローチの有効性を実証する。
論文 参考訳（メタデータ） (2022-08-12T17:03:50Z) - Extending Process Discovery with Model Complexity Optimization and
Cyclic States Identification: Application to Healthcare Processes [62.997667081978825]
モデル最適化のための半自動支援を実現するプロセスマイニング手法を提案する。
所望の粒度で生モデルを抽象化するモデル単純化手法が提案されている。
医療分野の異なるアプリケーションから得られた3つのデータセットを用いて、技術的ソリューションの能力を実証することを目的としている。
論文 参考訳（メタデータ） (2022-06-10T16:20:59Z) - Simulation of emergence in artificial societies: a practical model-based
approach with the EB-DEVS formalism [0.11470070927586014]
本稿では,創発特性のモデリング,シミュレーション,ライブ識別に適した新しいフォーマリズムであるEB-DEVSを適用する。
この研究は、コミュニケーション構造をモデル化するためのアプローチの簡潔さとコンパクトさに関するケーススタディ駆動の証拠を提供する。
論文 参考訳（メタデータ） (2021-10-15T15:55:16Z) - Lifted Model Checking for Relational MDPs [12.574454799055026]
pCTL-REBELは、リレーショナルMDP上のpCTL特性を検証するためのリフトモデルチェック手法である。
pCTLモデル検査手法は, 無限領域であっても, リレーショナルMDPに対して決定可能であることを示す。
論文 参考訳（メタデータ） (2021-06-22T13:12:36Z) - CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT
(Extended Version) [62.96267257163426]
我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。
まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。
次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
論文 参考訳（メタデータ） (2021-03-18T20:22:50Z) - S2RMs: Spatially Structured Recurrent Modules [105.0377129434636]
モジュール構造とテンポラル構造の両方を同時に活用できる動的構造を利用するための一歩を踏み出します。
我々のモデルは利用可能なビューの数に対して堅牢であり、追加のトレーニングなしで新しいタスクに一般化できる。
論文 参考訳（メタデータ） (2020-07-13T17:44:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。