論文の概要: A Verification Framework for Component-Based Modeling and Simulation
Putting the pieces together
- arxiv url: http://arxiv.org/abs/2301.03088v1
- Date: Sun, 8 Jan 2023 18:53:28 GMT
- ステータス: 処理完了
- システム内更新日: 2023-01-10 18:10:51.976325
- Title: A Verification Framework for Component-Based Modeling and Simulation
Putting the pieces together
- Title（参考訳）: 部品を組み立てたコンポーネントベースモデリングとシミュレーションのための検証フレームワーク
- Authors: Imran Mahmood
- Abstract要約: 提案する検証フレームワークは,コンポーザビリティを異なるレベルで検証するための方法,テクニック,ツールサポートを提供する。
特に、コンポーザビリティ全体の正しさにおける重要性と、プロセスで生じる困難度から、ダイナミック・セマンティック・コンポータビリティ(Dynamic-Semantic Composability)のレベルに注目します。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: In this thesis a comprehensive verification framework is proposed to contend
with some important issues in composability verification and a verification
process is suggested to verify composability of different kinds of systems
models, such as reactive, real-time and probabilistic systems. With an
assumption that all these systems are concurrent in nature in which different
composed components interact with each other simultaneously, the requirements
for the extensive techniques for the structural and behavioral analysis becomes
increasingly challenging. The proposed verification framework provides methods,
techniques and tool support for verifying composability at its different
levels. These levels are defined as foundations of consistent model
composability. Each level is discussed in detail and an approach is presented
to verify composability at that level. In particular we focus on the
Dynamic-Semantic Composability level due to its significance in the overall
composability correctness and also due to the level of difficulty it poses in
the process. In order to verify composability at this level we investigate the
application of three different approaches namely (i) Petri Nets based Algebraic
Analysis (ii) Colored Petri Nets (CPN) based State-space Analysis and (iii)
Communicating Sequential Processes based Model Checking. All three approaches
attack the problem of verifying dynamic-semantic composability in different
ways however they all share the same aim i.e., to confirm the correctness of a
composed model with respect to its requirement specifications.
- Abstract（参考訳）: 本論文では,構成可能性検証において重要な問題に対処する包括的検証フレームワークを提案し,反応性,リアルタイム性,確率性など,さまざまなシステムモデルの構成可能性を検証する検証プロセスを提案する。
これらのシステムはすべて、異なる構成されたコンポーネントが相互に同時に相互作用する性質において同時であるという仮定により、構造的および行動的分析のための広範な技術要件はますます困難になってきている。
提案する検証フレームワークは,コンポーザビリティを異なるレベルで検証するための方法,テクニック,ツールサポートを提供する。
これらのレベルは一貫性のあるモデル構成可能性の基礎として定義される。
それぞれのレベルが詳細に議論され、そのレベルで構成可能性を検証するアプローチが提示される。
特に、全体的なコンポーザビリティの正確性においてその重要性と、プロセスで生じる困難さによって、動的・意味論的コンポーザビリティのレベルに焦点をあてます。
このレベルで構成可能性を検証するために、3つの異なるアプローチの適用について検討する。
(i)ペトリネットに基づく代数解析
(ii)カラーペトリネット(cpn)に基づく状態空間解析と
(iii)逐次プロセスに基づくモデルチェックの伝達。
これら3つのアプローチは、動的意味的コンポーザビリティを異なる方法で検証する問題に対処するが、それらはすべて同じ目的、すなわち、要求仕様に関する合成モデルの正しさを確認するために共有する。
関連論文リスト
- SMLE: Safe Machine Learning via Embedded Overapproximation [4.129133569151574]
本研究は,デザイナ・ちょうせん特性を満たすことが保証される識別可能なMLモデルを訓練する作業について考察する。
現代のニューラルモデルにおけるコンプライアンスの厳格な検証と実施という計算複雑性のため、これは非常に難しい。
1)保守的なセマンティクスによる効率的な検証を可能にする汎用的,シンプルなアーキテクチャ。
回帰における線形不等式によって定義される特性と、多重ラベル分類における相互排他的クラスに対するアプローチを評価する。
論文 参考訳（メタデータ） (2024-09-30T17:19:57Z) - MARS: Benchmarking the Metaphysical Reasoning Abilities of Language Models with a Multi-task Evaluation Dataset [50.36095192314595]
大きな言語モデル(LLM)は、一般化可能な推論能力を持つ意識的なエージェントとして機能する。
この能力は、イベントにおける無限の可能な変更をモデル化する複雑さのために、まだ探索されていない。
我々は,各ステップに対応する3つのタスクからなる最初のベンチマークMARSを紹介する。
論文 参考訳（メタデータ） (2024-06-04T08:35:04Z) - OSM: Leveraging Model Checking for Observing Dynamic 1 behaviors in
Aspect-Oriented Applications [0.0]
観測ベース統計モデルチェック(OSM)フレームワークは、基本的なシステムコードから直接実行可能な形式モデルを構築するために開発された。
これにより、プリコンディションシフト中の電子健康記録システムの未収量性能が保証される。
論文 参考訳（メタデータ） (2024-03-03T00:03:34Z) - Object-Centric Conformance Alignments with Synchronization (Extended Version) [57.76661079749309]
対象中心のペトリネットが一対多の関係を捉える能力と,その同一性に基づいたオブジェクトの比較と同期を行う識別子を持つペトリネットの能力を組み合わせた,新たな形式主義を提案する。
我々は、満足度変調理論(SMT)の符号化に基づく、そのようなネットに対する適合性チェック手法を提案する。
論文 参考訳（メタデータ） (2023-12-13T21:53:32Z) - Variable Importance Matching for Causal Inference [73.25504313552516]
これらの目標を達成するためのModel-to-Matchと呼ばれる一般的なフレームワークについて説明する。
Model-to-Matchは、距離メートル法を構築するために変数重要度測定を使用する。
LASSO を用いて Model-to-Match フレームワークを運用する。
論文 参考訳（メタデータ） (2023-02-23T00:43:03Z) - Universal Information Extraction as Unified Semantic Matching [54.19974454019611]
情報抽出を,異なるタスクやスキーマで共有される構造化と概念化という,2つの能力に分割する。
このパラダイムに基づいて、統一意味マッチングフレームワークを用いて様々なIEタスクを普遍的にモデル化することを提案する。
このように、USMはスキーマと入力テキストを共同でエンコードし、サブ構造を一様に並列に抽出し、必要に応じてターゲット構造を制御できる。
論文 参考訳（メタデータ） (2023-01-09T11:51:31Z) - Relational Action Bases: Formalization, Effective Safety Verification,
and Invariants (Extended Version) [67.99023219822564]
我々はリレーショナルアクションベース(RAB)の一般的な枠組みを紹介する。
RABは両方の制限を解除することで既存のモデルを一般化する。
データ対応ビジネスプロセスのベンチマークにおいて、このアプローチの有効性を実証する。
論文 参考訳（メタデータ） (2022-08-12T17:03:50Z) - Exploring the Trade-off between Plausibility, Change Intensity and
Adversarial Power in Counterfactual Explanations using Multi-objective
Optimization [73.89239820192894]
自動対物生成は、生成した対物インスタンスのいくつかの側面を考慮すべきである。
本稿では, 対実例生成のための新しい枠組みを提案する。
論文 参考訳（メタデータ） (2022-05-20T15:02:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。