論文の概要: 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の両方のデプロイメントのランタイム検証を提供し、システムパフォーマンスとスケーラビリティの強化を自動化するために、自分自身を必須のオープンソースリソースとして位置づける。
関連論文リスト
- Enhanced Transformer architecture for in-context learning of dynamical systems [0.3749861135832073]
本稿では,従来のメタモデリングフレームワークを3つの重要な革新を通じて強化する。
これらの修正の有効性は、Wiener-Hammerstein系クラスに焦点をあてた数値的な例を通して示される。
論文 参考訳（メタデータ） (2024-10-04T10:05:15Z) - A process algebraic framework for multi-agent dynamic epistemic systems [55.2480439325792]
本稿では,マルチエージェント,知識ベース,動的システムのモデリングと解析のための統合フレームワークを提案する。
モデリング側では,このようなフレームワークを実用的な目的に使いやすくするプロセス代数的,エージェント指向の仕様言語を提案する。
論文 参考訳（メタデータ） (2024-07-24T08:35:50Z) - Benchmarks as Microscopes: A Call for Model Metrology [76.64402390208576]
現代の言語モデル(LM)は、能力評価において新たな課題を提起する。
メトリクスに自信を持つためには、モデルミアロジの新たな規律が必要です。
論文 参考訳（メタデータ） (2024-07-22T17:52:12Z) - Process Modeling With Large Language Models [42.0652924091318]
本稿では,大規模言語モデル(LLM)のプロセスモデリングへの統合について検討する。
プロセスモデルの自動生成と反復的改善にLLMを利用するフレームワークを提案する。
予備的な結果は、プロセスモデリングタスクを合理化するフレームワークの能力を示している。
論文 参考訳（メタデータ） (2024-03-12T11:27:47Z) - Probabilistic ML Verification via Weighted Model Integration [11.812078181471634]
機械学習モデルの確率形式検証(PFV)はその初期段階にある。
重み付きモデル統合(WMI)に基づくMLシステムのPFV統合フレームワークを提案する。
ML検証文献におけるスケーリング手法が,本来の範囲を超えていかに一般化できるかを示す。
論文 参考訳（メタデータ） (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) - 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) - Lifted Model Checking for Relational MDPs [12.574454799055026]
pCTL-REBELは、リレーショナルMDP上のpCTL特性を検証するためのリフトモデルチェック手法である。
pCTLモデル検査手法は, 無限領域であっても, リレーショナルMDPに対して決定可能であることを示す。
論文 参考訳（メタデータ） (2021-06-22T13:12:36Z) - S2RMs: Spatially Structured Recurrent Modules [105.0377129434636]
モジュール構造とテンポラル構造の両方を同時に活用できる動的構造を利用するための一歩を踏み出します。
我々のモデルは利用可能なビューの数に対して堅牢であり、追加のトレーニングなしで新しいタスクに一般化できる。
論文 参考訳（メタデータ） (2020-07-13T17:44:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。