論文の概要: Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing

• arxiv url: http://arxiv.org/abs/2501.12932v3
• Date: Mon, 27 Oct 2025 13:16:43 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-28 17:41:21.368695
• Title: Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing
• Title（参考訳）: オーバーホールを伴う契約オートマタ環境の形式的解析--モデリング,検証,テスト
• Authors: Davide Basile,
• Abstract要約: 契約オートマトン環境(CARE)と呼ばれる分散ランタイムアプリケーションは、有限状態オートマトン方言を用いて指定されたサービスアプリケーションを実現するために導入された。 我々はCAREの正式なモデリング、検証、テストについて詳述する。
• 参考スコア（独自算出の注目度）: 0.11844977816228043
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Recently, a distributed middleware application called contract automata runtime environment (CARE) has been introduced to realise service applications specified using a dialect of finite-state automata. In this paper, we detail the formal modelling, verification and testing of CARE. We provide a formalisation as a network of stochastic timed automata. The model is verified against the desired properties with the tool Uppaal, utilising exhaustive and statistical model checking techniques. Abstract tests are generated from the Uppaal models that are concretised for testing CARE. This research emphasises the advantages of employing formal modelling, verification and testing processes to enhance the dependability of an open-source distributed application. We discuss the methodology used for modelling the application and generating concrete tests from the abstract model, addressing the issues that have been identified and fixed.
• Abstract（参考訳）: 近年,契約自動実行環境(CARE)と呼ばれる分散ミドルウェアアプリケーションが登場し,有限状態オートマトンを用いたサービスアプリケーションを実現している。 本稿では,CAREの形式的モデリング,検証,試験について述べる。 確率的時間自動のネットワークとして形式化を提供する。 モデルはUppaalツールで望ましい特性に対して検証され、徹底的および統計的モデル検査技術を利用する。 抽象テストは、CAREをテストするために考案されたUppaalモデルから生成される。 本研究は、オープンソースの分散アプリケーションの信頼性を高めるために、フォーマルなモデリング、検証、テストプロセスを採用する利点を強調している。 アプリケーションをモデル化し、抽象モデルから具体的なテストを生成するための方法論について議論し、特定され、修正された問題に対処する。

関連論文リスト

• Tool-Assisted Conformance Checking to Reference Process Models [0.9117519504551699]
  整合性チェックは、さまざまなプロセスの品質と一貫性を維持するために不可欠です。 本稿では,参照モデルに対する具体的なプロセスモデルの自動適合性チェックについて検討する。
  論文  参考訳（メタデータ） (2025-08-01T16:08:24Z)
• MBTModelGenerator: A software tool for reverse engineering of Model-based Testing (MBT) models from clickstream data of web applications [1.516251872371896]
  このツールはUIイベントをキャプチャして状態遷移モデルに変換し、その結果をGraphWalker MBTツールと互換性のあるフォーマットでエクスポートする。 本報告では, システム要件, 設計決定, 実装詳細, テストプロセス, ツールの実証評価について報告する。
  論文  参考訳（メタデータ） (2025-06-09T19:44:10Z)
• Sample, Don't Search: Rethinking Test-Time Alignment for Language Models [55.2480439325792]
  新しいテストタイムアライメントアプローチであるQAlignを紹介します。 テスト時間計算をスケールする際、QAlignは各プロンプトの最適配向分布からのサンプリングに収束する。 マルコフ連鎖モンテカルロのテキスト生成における最近の進歩を取り入れることで、基礎となるモデルを変更したり、ロジットアクセスを必要とせずに、より良い整合出力を可能にする。
  論文  参考訳（メタデータ） (2025-04-04T00:41:40Z)
• Thinking Longer, Not Larger: Enhancing Software Engineering Agents via Scaling Test-Time Compute [61.00662702026523]
  より大規模なモデルではなく、推論時間の増加を活用する統合されたテスト時間計算スケーリングフレームワークを提案する。 当社のフレームワークには,内部TTCと外部TTCの2つの補完戦略が組み込まれている。 当社の textbf32B モデルは,DeepSeek R1 671B や OpenAI o1 など,はるかに大きなモデルを上回る 46% の課題解決率を実現している。
  論文  参考訳（メタデータ） (2025-03-31T07:31:32Z)
• Contract Based Program Models for Software Model Checking [0.0]
  構成モデル検査のために以前に開発された形式主義を提案する。 InCで書かれた組込み型安全クリティカルソフトウェアにおいて,提案する検証手法をサポートするために,作業フローとツールチェーンの構想について述べる。
  論文  参考訳（メタデータ） (2025-03-14T09:34:59Z)
• Neural Model Checking [10.376573742987917]
  時間論理をモデル化するための機械学習手法を導入し,ハードウェアの形式的検証に適用する。 我々の新しいアプローチは、ニューラルネットワークを線形時間論理の形式証明証明として用いることによって、機械学習と記号推論を組み合わせる。 提案手法は,SystemVerilogで記述された標準的なハードウェア設計において,最先端の学術的,商業的なモデルチェッカーよりも優れていることを示す。
  論文  参考訳（メタデータ） (2024-10-31T10:17:04Z)
• Model Equality Testing: Which Model Is This API Serving? [59.005869726179455]
  2サンプルテスト問題であるモデル品質テストのような歪みの検出を形式化する。 単純な文字列カーネル上に構築されたテストは、歪みの範囲に対して77.4%の中央値を達成する。 次に、このテストを4つのLlamaモデルの商用推論APIに適用し、31のエンドポイントのうち11がMetaがリリースしたリファレンスウェイトとは異なる分布を提供することがわかった。
  論文  参考訳（メタデータ） (2024-10-26T18:34:53Z)
• Automatic Generation of Behavioral Test Cases For Natural Language Processing Using Clustering and Prompting [6.938766764201549]
  本稿では,大規模言語モデルと統計的手法の力を活用したテストケースの自動開発手法を提案する。 4つの異なる分類アルゴリズムを用いて行動テストプロファイルを分析し、それらのモデルの限界と強みについて議論する。
  論文  参考訳（メタデータ） (2024-07-31T21:12:21Z)
• Type-level Property Based Testing [0.0]
  本稿では,ソフトウェア仕様と依存型付けモデル,コンパイル時の実装の結合を統一する自動フレームワークを提案する。 いくつかの興味深いシステムやネットワークプロトコルをモデル化し、型チェッカーで実装が指定された動作であることを検証し、モデルが仕様のセマンティクスにマッチしていることをテストすることができます。
  論文  参考訳（メタデータ） (2024-07-17T16:43:41Z)
• Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
  本稿では,学習されたタイムドオートマトンとシステムに関する公式知識グラフを組み合わせることで,CPPSのモデルベース異常検出を改善することを目的とする。 モデルと検出された異常の両方を知識グラフに記述し、モデルと検出された異常をより容易に解釈できるようにする。
  論文  参考訳（メタデータ） (2023-08-25T15:25:57Z)
• Formal Verification Of A Shopping Basket Application Model Using PRISM [0.0]
  ショッピング・バスケット・アプリケーション・モデルにおけるPrism Model Checkerを用いたシミュレーションの結果を示す。 目的は、買い物客が買い物プロセスの多くの定義された状態を通過するときの行動をシミュレートすることである。
  論文  参考訳（メタデータ） (2023-07-16T00:14:40Z)
• Exploring validation metrics for offline model-based optimisation with diffusion models [50.404829846182764]
  モデルベース最適化(MBO)では、マシンラーニングを使用して、(基底真理)オラクルと呼ばれるブラックボックス関数に対する報酬の尺度を最大化する候補を設計することに興味があります。 モデル検証中に基底オラクルに対する近似をトレーニングし、その代わりに使用することができるが、その評価は近似的であり、敵の例に対して脆弱である。 本手法は,外挿量を測定するために提案した評価フレームワークにカプセル化されている。
  論文  参考訳（メタデータ） (2022-11-19T16:57:37Z)
• Model ensemble instead of prompt fusion: a sample-specific knowledge transfer method for few-shot prompt tuning [85.55727213502402]
  我々は、ソースタスクのソフトプロンプトから知識を伝達することで、プロンプトチューニングにおける数ショットのパフォーマンスを改善することに集中する。 我々はソースモデル(SESoM)のサンプル固有アンサンブルを提案する。 SESoMは、ソースモデルが出力されるときに、ターゲットの各サンプルに対するソースモデルのコントリビューションを個別に調整することを学ぶ。
  論文  参考訳（メタデータ） (2022-10-23T01:33:16Z)
• Generalization Properties of Retrieval-based Models [50.35325326050263]
  検索ベースの機械学習手法は、幅広い問題で成功をおさめた。 これらのモデルの約束を示す文献が増えているにもかかわらず、そのようなモデルの理論的基盤はいまだに解明されていない。 本稿では,その一般化能力を特徴付けるために,検索ベースモデルの形式的処理を行う。
  論文  参考訳（メタデータ） (2022-10-06T00:33:01Z)
• Learning to Generalize across Domains on Single Test Samples [126.9447368941314]
  単体テストサンプルでドメインをまたいで一般化することを学ぶ。 変分ベイズ推論問題として単検体への適応を定式化する。 我々のモデルは、ドメインの一般化のための複数のベンチマークにおいて、最先端のメソッドよりも少なくとも同等で、より優れたパフォーマンスを達成します。
  論文  参考訳（メタデータ） (2022-02-16T13:21:04Z)
• Automated simulation and verification of process models discovered by process mining [0.0]
  本稿では,プロセスマイニング技術を用いたプロセスモデルの自動解析手法を提案する。 プロセスマイニングは、さまざまなデバイスによって生成されたイベントデータに隠された、基盤となるプロセスを探索する。
  論文  参考訳（メタデータ） (2020-11-03T11:51:53Z)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。