論文の概要: Quantitative Assurance and Synthesis of Controllers from Activity
Diagrams
- arxiv url: http://arxiv.org/abs/2403.00169v1
- Date: Thu, 29 Feb 2024 22:40:39 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-05 18:56:57.782696
- Title: Quantitative Assurance and Synthesis of Controllers from Activity
Diagrams
- Title（参考訳）: 活動図からの制御器の量的保証と合成
- Authors: Kangfeng Ye, Fang Yan, Simos Gerasimou
- Abstract要約: 確率的モデル検査は、定性的および定量的な性質を自動検証するために広く用いられている形式的検証手法である。
これにより、必要な知識を持っていない研究者やエンジニアにはアクセスできない。
本稿では,確率時間の新しいプロファイル,品質アノテーション,3つのマルコフモデルにおけるADの意味論的解釈,アクティビティ図からPRISM言語への変換ルールのセットなど,ADの総合的な検証フレームワークを提案する。
最も重要なことは、モデルをベースとした手法を用いて、完全自動検証のための変換アルゴリズムを開発し、QASCADと呼ばれるツールで実装したことです。
- 参考スコア（独自算出の注目度）: 4.419843514606336
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Probabilistic model checking is a widely used formal verification technique
to automatically verify qualitative and quantitative properties for
probabilistic models. However, capturing such systems, writing corresponding
properties, and verifying them require domain knowledge. This makes it not
accessible for researchers and engineers who may not have the required
knowledge. Previous studies have extended UML activity diagrams (ADs),
developed transformations, and implemented accompanying tools for automation.
The research, however, is incomprehensive and not fully open, which makes it
hard to be evaluated, extended, adapted, and accessed. In this paper, we
propose a comprehensive verification framework for ADs, including a new profile
for probability, time, and quality annotations, a semantics interpretation of
ADs in three Markov models, and a set of transformation rules from activity
diagrams to the PRISM language, supported by PRISM and Storm. Most importantly,
we developed algorithms for transformation and implemented them in a tool,
called QASCAD, using model-based techniques, for fully automated verification.
We evaluated one case study where multiple robots are used for delivery in a
hospital and further evaluated six other examples from the literature. With all
these together, this work makes noteworthy contributions to the verification of
ADs by improving evaluation, extensibility, adaptability, and accessibility.
- Abstract（参考訳）: 確率モデル検査は、確率モデルに対する定性的および定量的特性を自動的に検証するために広く用いられている形式的検証手法である。
しかし、そのようなシステムをキャプチャし、対応するプロパティを書き、検証するにはドメイン知識が必要です。
これにより、必要な知識を持っていない研究者やエンジニアにはアクセスできない。
これまでの研究では、UMLアクティビティダイアグラム(AD)を拡張し、トランスフォーメーションを開発し、自動化のためのツールを実装してきた。
しかし、この研究は理解できず、完全には公開されていないため、評価、拡張、適応、アクセスが困難である。
本稿では、確率、時間、品質アノテーションの新しいプロファイル、マルコフモデルにおけるADの意味論的解釈、PRISMとStormがサポートするアクティビティ図からPRISM言語への変換ルールのセットを含む、ADの総合的な検証フレームワークを提案する。
最も重要なことは、モデルをベースとした手法を用いて、完全自動検証のための変換アルゴリズムを開発し、QASCADと呼ばれるツールで実装したことです。
病院での配送に複数のロボットが使用されるケーススタディを1例評価し,さらに6例を文献から評価した。
これらすべてを合わせて、評価、拡張性、適応性、アクセシビリティを改善して、ADの検証に注目すべき貢献をする。
関連論文リスト
- Automatic Generation of Behavioral Test Cases For Natural Language Processing Using Clustering and Prompting [6.938766764201549]
本稿では,大規模言語モデルと統計的手法の力を活用したテストケースの自動開発手法を提案する。
4つの異なる分類アルゴリズムを用いて行動テストプロファイルを分析し、それらのモデルの限界と強みについて議論する。
論文 参考訳（メタデータ） (2024-07-31T21:12:21Z) - KGValidator: A Framework for Automatic Validation of Knowledge Graph Construction [2.9526207670430384]
生成モデルを用いて知識グラフを検証する場合に,一貫性と検証のためのフレームワークを導入する。
この設計は適応と拡張が容易で、どんなグラフ構造化データでも検証することができる。
論文 参考訳（メタデータ） (2024-04-24T15:27:25Z) - AIDE: An Automatic Data Engine for Object Detection in Autonomous Driving [68.73885845181242]
本稿では,問題を自動的に識別し,データを効率よくキュレートし,自動ラベル付けによりモデルを改善する自動データエンジン(AIDE)を提案する。
さらに,AVデータセットのオープンワールド検出のためのベンチマークを構築し,様々な学習パラダイムを包括的に評価し,提案手法の優れた性能を低コストで実証する。
論文 参考訳（メタデータ） (2024-03-26T04:27:56Z) - Towards Automatic Translation of Machine Learning Visual Insights to
Analytical Assertions [23.535630175567146]
機械学習(ML)の可視化で観察される視覚特性をPythonアサーションに変換する自動化ツールを開発するためのビジョンを提示する。
このツールは、ML開発サイクルでこれらの視覚化を手作業で検証するプロセスの合理化を目的としている。
論文 参考訳（メタデータ） (2024-01-15T14:11:59Z) - QualEval: Qualitative Evaluation for Model Improvement [82.73561470966658]
モデル改善のための手段として,自動定性評価による定量的スカラー指標を付加するQualEvalを提案する。
QualEvalは強力なLCM推論器と新しいフレキシブルリニアプログラミングソルバを使用して、人間の読みやすい洞察を生成する。
例えば、その洞察を活用することで、Llama 2モデルの絶対性能が最大15%向上することを示す。
論文 参考訳（メタデータ） (2023-11-06T00:21:44Z) - FIND: A Function Description Benchmark for Evaluating Interpretability
Methods [86.80718559904854]
本稿では,自動解釈可能性評価のためのベンチマークスイートであるFIND(Function Interpretation and Description)を紹介する。
FINDには、トレーニングされたニューラルネットワークのコンポーネントに似た機能と、私たちが生成しようとしている種類の記述が含まれています。
本研究では、事前訓練された言語モデルを用いて、自然言語とコードにおける関数の振る舞いの記述を生成する手法を評価する。
論文 参考訳（メタデータ） (2023-09-07T17:47:26Z) - Scaling up Memory-Efficient Formal Verification Tools for Tree Ensembles [2.588973722689844]
ツール記述として提示されたVoTEアルゴリズムを形式化し拡張する。
コア検証エンジンからプロパティチェックを分離することで、汎用性のある要件の検証が可能となります。
数値認識と航空機衝突回避という2つのケーススタディで、このツールの適用を実証します。
論文 参考訳（メタデータ） (2021-05-06T11:50:22Z) - DirectDebug: Automated Testing and Debugging of Feature Models [55.41644538483948]
変数モデル(例えば、特徴モデル)は、ソフトウェアアーティファクトの変数と共通性を表現する一般的な方法である。
複雑でしばしば大規模な機能モデルは欠陥になりうる、すなわち、ソフトウェアアーチファクトの期待される変動特性を表現しない。
論文 参考訳（メタデータ） (2021-02-11T11:22:20Z) - Few-Shot Named Entity Recognition: A Comprehensive Study [92.40991050806544]
マルチショット設定のモデル一般化能力を向上させるための3つの手法を検討する。
ラベル付きデータの比率の異なる10の公開nerデータセットについて経験的比較を行う。
マルチショットとトレーニングフリーの両方の設定で最新の結果を作成します。
論文 参考訳（メタデータ） (2020-12-29T23:43:16Z) - IFC models for (semi)automating common planning checks for building
permits [0.0]
IFCモデルから必要な情報を抽出して代表規則をチェックするツールが開発された。
ケーススタディは、場所、規制、入力モデルに特化していますが、遭遇した問題のタイプは、自動コードコンプライアンスチェックの一般的な例です。
論文 参考訳（メタデータ） (2020-11-03T15:29:47Z) - Universal Source-Free Domain Adaptation [57.37520645827318]
ドメイン適応のための新しい2段階学習プロセスを提案する。
Procurementの段階では、今後のカテゴリギャップやドメインシフトに関する事前知識を前提とせず、将来的なソースフリーデプロイメントのためのモデルの提供を目標としています。
Deploymentの段階では、幅広いカテゴリギャップをまたいで動作可能な統一適応アルゴリズムを設計することを目的としている。
論文 参考訳（メタデータ） (2020-04-09T07:26:20Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。