Fugu-MT 論文翻訳(概要): Formal Verification Of A Shopping Basket Application Model Using PRISM

論文の概要: Formal Verification Of A Shopping Basket Application Model Using PRISM

arxiv url: http://arxiv.org/abs/2308.00618v1
Date: Sun, 16 Jul 2023 00:14:40 GMT
ステータス: 処理完了
システム内更新日: 2023-10-23 15:41:36.910649
Title: Formal Verification Of A Shopping Basket Application Model Using PRISM
Title（参考訳）: prismを用いた買い物かごアプリケーションモデルの形式検証
Authors: Patrick Mukala
Abstract要約: ショッピング・バスケット・アプリケーション・モデルにおけるPrism Model Checkerを用いたシミュレーションの結果を示す。目的は、買い物客が買い物プロセスの多くの定義された状態を通過するときの行動をシミュレートすることである。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by/4.0/
Abstract: Formal verification is at the heart of model validation and correctness. With model checking, invaluable realizations have been accomplished in software engineering and particularly in software development. By means of this approach, complex applications can be simulated and their performance forecasted in light with requirements at hands and expected performance. In this short paper we present the results of a simulation using Prism Model Checker for a Shopping Basket Application Model. Applied on a modified model from a projected process model, the objective is to simulate the behavior of shoppers as they go through a number of defined states of the shopping process and express accessibility and reachability through a number of defined properties.
Abstract（参考訳）: 形式的検証はモデル検証と正確性の中心にある。モデルチェックでは、ソフトウェア工学、特にソフトウェア開発において、重要な実現がなされている。このアプローチにより、複雑なアプリケーションをシミュレートし、そのパフォーマンスは、手元にある要件と期待するパフォーマンスと合致して予測される。本稿では,Prism Model Checker を用いたショッピング・バスケット・アプリケーション・モデルにおけるシミュレーション結果について述べる。プロジェクテッドプロセスモデルから修正されたモデルに適用することで、買い物客の振る舞いをシミュレートし、ショッピングプロセスのいくつかの定義された状態を経て、複数の定義されたプロパティを通してアクセシビリティと到達可能性を表現する。

関連論文リスト

Towards Synthetic Trace Generation of Modeling Operations using In-Context Learning Approach [1.8874331450711404]
本稿では,イベントログのモデリング,インテリジェントなモデリングアシスタント,モデリング操作の生成を組み合わせた概念的フレームワークを提案する。特に、アーキテクチャは、設計者がシステムを指定するのを助け、その操作をグラフィカルなモデリング環境内で記録し、関連する操作を自動的に推奨する、モデリングコンポーネントから構成される。
論文参考訳（メタデータ） (2024-08-26T13:26:44Z)
Semantic Capability Model for the Simulation of Manufacturing Processes [38.69817856379812]
シミュレーションは製造工程の検査の機会を提供する。異なるシミュレーションの組み合わせは、あるシミュレーションの出力が別のシミュレーションの入力パラメータとして機能し、結果として一連のシミュレーションとなるときに必要である。シミュレーション、特定の知識を生成する能力、それぞれの品質基準を表現した情報モデルが導入された。
論文参考訳（メタデータ） (2024-08-15T09:28:08Z)
Mining Constraints from Reference Process Models for Detecting Best-Practice Violations in Event Log [1.389948527681755]
本稿では,参照モデルコレクションから宣言的ベストプラクティス制約をマイニングするためのフレームワークを提案する。本稿では,実世界のプロセスモデルコレクションとイベントログに基づく評価により,ベストプラクティス違反を検出するフレームワークの能力を実証する。
論文参考訳（メタデータ） (2024-07-02T15:05:37Z)
Verifiable evaluations of machine learning models using zkSNARKs [40.538081946945596]
本研究は,zkSNARKによるモデル推論を用いたモデル評価の検証手法を提案する。結果として得られたデータセット上のモデル出力のゼロ知識計算証明は、検証可能な評価証明にパッケージ化することができる。実世界のモデルのサンプルでこれを初めてデモし、重要な課題と設計ソリューションを強調します。
論文参考訳（メタデータ） (2024-02-05T02:21:11Z)
Earning Extra Performance from Restrictive Feedbacks [41.05874087063763]
モデルチューニング問題の形式を記述するために,rerestriCTive feeddbacks (EXPECTED) から emphEarning eXtra PerformancE という課題を設定した。モデルプロバイダの目標は、最終的にフィードバックを利用することで、ローカルユーザに対して満足のいくモデルを提供することです。本稿では,パラメータ分布を探索し,モデルパラメータに関するモデル性能の幾何を特徴付けることを提案する。
論文参考訳（メタデータ） (2023-04-28T13:16:54Z)
Exploring validation metrics for offline model-based optimisation with diffusion models [50.404829846182764]
モデルベース最適化(MBO)では、マシンラーニングを使用して、(基底真理)オラクルと呼ばれるブラックボックス関数に対する報酬の尺度を最大化する候補を設計することに興味があります。モデル検証中に基底オラクルに対する近似をトレーニングし、その代わりに使用することができるが、その評価は近似的であり、敵の例に対して脆弱である。本手法は,外挿量を測定するために提案した評価フレームワークにカプセル化されている。
論文参考訳（メタデータ） (2022-11-19T16:57:37Z)
Extending Process Discovery with Model Complexity Optimization and Cyclic States Identification: Application to Healthcare Processes [62.997667081978825]
モデル最適化のための半自動支援を実現するプロセスマイニング手法を提案する。所望の粒度で生モデルを抽象化するモデル単純化手法が提案されている。医療分野の異なるアプリケーションから得られた3つのデータセットを用いて、技術的ソリューションの能力を実証することを目的としている。
論文参考訳（メタデータ） (2022-06-10T16:20:59Z)
On the Limits of Evaluating Embodied Agent Model Generalization Using Validation Sets [101.28658250723804]
本稿では,より広い視野を効果的に活用し,次のステップでナビゲーションや操作を行うかを選択するモジュールによるトランスフォーマーモデルの拡張実験を行う。提案したモジュールは改良され,実際に,一般的なベンチマークデータセットであるALFREDの未確認検証セット上での最先端のパフォーマンスが向上した。この結果は、機械学習タスクではより広い現象かもしれないが、主にテストスプリットの評価を制限するベンチマークでのみ顕著である、と我々は考えているので強調する。
論文参考訳（メタデータ） (2022-05-18T23:52:21Z)
How to Design Sample and Computationally Efficient VQA Models [53.65668097847456]
テキストを確率的プログラムとして表現し,イメージをオブジェクトレベルのシーングラフとして表現することが,これらのデシラタを最も満足していることが判明した。既存のモデルを拡張して,これらのソフトプログラムとシーングラフを活用して,エンドツーエンドで質問応答ペアをトレーニングします。
論文参考訳（メタデータ） (2021-03-22T01:48:16Z)
DirectDebug: Automated Testing and Debugging of Feature Models [55.41644538483948]
変数モデル(例えば、特徴モデル)は、ソフトウェアアーティファクトの変数と共通性を表現する一般的な方法である。複雑でしばしば大規模な機能モデルは欠陥になりうる、すなわち、ソフトウェアアーチファクトの期待される変動特性を表現しない。
論文参考訳（メタデータ） (2021-02-11T11:22:20Z)
Model Reuse with Reduced Kernel Mean Embedding Specification [70.044322798187]
現在のアプリケーションで有用なモデルを見つけるための2段階のフレームワークを提案する。アップロードフェーズでは、モデルがプールにアップロードされている場合、モデルの仕様としてカーネル平均埋め込み(RKME)を縮小する。デプロイフェーズでは、RKME仕様の値に基づいて、現在のタスクと事前訓練されたモデルの関連性を測定する。
論文参考訳（メタデータ） (2020-01-20T15:15:07Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。