論文の概要: Runtime Verification on Abstract Finite State Models

• arxiv url: http://arxiv.org/abs/2406.12715v1
• Date: Tue, 18 Jun 2024 15:32:31 GMT
• ステータス: 処理完了
• システム内更新日: 2024-06-19 18:18:55.596707
• Title: Runtime Verification on Abstract Finite State Models
• Title（参考訳）: 抽象有限状態モデルによる実行時検証
• Authors: KP Jevitha, Bharat Jayaraman, M Sethumadhavan,
• Abstract要約: マルチスレッドJavaプログラムの実行から有限状態モデルを抽出する方法を示し、精度特性のランタイム検証を実行する。 本論文の主な貢献は,プロパティ保存抽象モデルのオンラインプロパティチェックを通じて,実行時検証の効率性を示すことである。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Finite-state models are ubiquitous in the study of concurrent systems, especially controllers and servers that operate in a repetitive cycle. In this paper, we show how to extract finite state models from a run of a multi-threaded Java program and carry out runtime verification of correctness properties. These properties include data-oriented and control-oriented properties; the former express correctness conditions over the data fields of objects, while the latter are concerned with the correct flow of control among the modules of larger software. As the extracted models can become very large for long runs, the focus of this paper is on constructing reduced models with user-defined abstraction functions that map a larger domain space to a smaller one. The abstraction functions should be chosen so that the resulting model is property preserving, i.e., proving a property on the abstract model carries over to the concrete model. The main contribution of this paper is in showing how runtime verification can be made efficient through online property checking on property-preserving abstract models. The property specification language resembles a propositional linear temporal logic augmented with simple datatypes and operators. Classic concurrency examples and larger case studies (Multi-rotor Drone Controller, OAuth Protocol) are presented in order to demonstrate the usefulness of our proposed techniques, which are incorporated in an Eclipse plug-in for runtime visualization and verification of Java programs.
• Abstract（参考訳）: 有限状態モデルは並列システム、特に反復サイクルで動作するコントローラやサーバの研究においてユビキタスである。 本稿では,マルチスレッドJavaプログラムの実行から有限状態モデルを抽出し,精度特性のランタイム検証を行う方法について述べる。 これらの特性には、データ指向および制御指向の特性が含まれており、前者はオブジェクトのデータフィールド上での表現正当性条件を示し、後者はより大きなソフトウェアモジュール間での制御の正しいフローに関するものである。 抽出されたモデルは長期にわたって非常に大きくなりうるため、この論文の焦点は、より大きなドメイン空間をより小さなドメイン空間にマッピングするユーザ定義の抽象関数を持つ縮小モデルの構築である。 抽象関数は、結果のモデルがプロパティ保存であるように選択されるべきである。 本論文の主な貢献は,プロパティ保存抽象モデルのオンラインプロパティチェックを通じて,実行時検証の効率性を示すことである。 プロパティ仕様言語は、単純なデータ型と演算子で拡張された命題線形時間論理に似ている。 従来の並列処理の例とより大きなケーススタディ(Multi-rotor Drone Controller, OAuth Protocol)を提示し,Javaプログラムの実行時ビジュアライゼーションと検証のためのEclipseプラグインに組み込まれた提案手法の有用性を実証した。

関連論文リスト

• EmbedLLM: Learning Compact Representations of Large Language Models [28.49433308281983]
  大規模言語モデルのコンパクトなベクトル表現を学習するためのフレームワークである EmbedLLM を提案する。 このような埋め込みを学習するためのエンコーダ-デコーダアプローチと,その有効性を評価するための体系的なフレームワークを導入する。 EmbedLLMはモデルルーティングにおいて,精度とレイテンシの両方において,従来の手法よりも優れていた。
  論文  参考訳（メタデータ） (2024-10-03T05:43:24Z)
• Fine-Tuning Enhances Existing Mechanisms: A Case Study on Entity Tracking [53.66999416757543]
  本研究では,微調整が言語モデルに実装された内部メカニズムに与える影響について検討する。 微調整はモデルの機械的操作を変えるのではなく、強化する。
  論文  参考訳（メタデータ） (2024-02-22T18:59:24Z)
• Formal Verification Of A Shopping Basket Application Model Using PRISM [0.0]
  ショッピング・バスケット・アプリケーション・モデルにおけるPrism Model Checkerを用いたシミュレーションの結果を示す。 目的は、買い物客が買い物プロセスの多くの定義された状態を通過するときの行動をシミュレートすることである。
  論文  参考訳（メタデータ） (2023-07-16T00:14:40Z)
• DORE: Document Ordered Relation Extraction based on Generative Framework [56.537386636819626]
  本稿では,既存のDocREモデルの根本原因について検討する。 本稿では,モデルが学習しやすく,決定論的な関係行列から記号列と順序列を生成することを提案する。 4つのデータセットに対する実験結果から,提案手法は生成型DocREモデルの性能を向上させることができることが示された。
  論文  参考訳（メタデータ） (2022-10-28T11:18:10Z)
• Segmenting Moving Objects via an Object-Centric Layered Representation [100.26138772664811]
  深層表現を用いたオブジェクト中心セグメンテーションモデルを提案する。 複数のオブジェクトで合成トレーニングデータを生成するスケーラブルなパイプラインを導入する。 標準的なビデオセグメンテーションベンチマークでモデルを評価する。
  論文  参考訳（メタデータ） (2022-07-05T17:59:43Z)
• SAT-Based Extraction of Behavioural Models for Java Libraries with Collections [0.087024326813104]
  振る舞いモデルは、ソフトウェア検証、テスト、監視、公開などのための貴重なツールです。 ソフトウェア開発者によって提供されることはめったになく、ソースまたはコンパイルされたコードから抽出されなければならない。 これらのアプローチのほとんどは、コンパイルされたバイトコードの分析に依存します。 我々はJavaソースコードから有限状態マシン(FSM)の形式で振る舞いモデルを取り出して、取得したFSMがソフトウェア開発者によって容易に理解できるようにしたいと思っています。
  論文  参考訳（メタデータ） (2022-05-30T17:27:13Z)
• Visualising Deep Network's Time-Series Representations [93.73198973454944]
  機械学習モデルの普及にもかかわらず、多くの場合、モデルの内部で起きていることに関する洞察のないブラックボックスとして運用される。 本稿では,多次元時系列データの可視化に着目し,この問題に対処する手法を提案する。 高周波在庫市場データセットの実験は、この方法が迅速かつ識別可能な可視化を提供することを示しています。
  論文  参考訳（メタデータ） (2021-03-12T09:53:34Z)
• Model-Invariant State Abstractions for Model-Based Reinforcement Learning [54.616645151708994]
  textitmodel-invarianceという新しいタイプの状態抽象化を紹介します。 これにより、状態変数の見当たらない値の新しい組み合わせへの一般化が可能になる。 このモデル不変状態抽象化を通じて最適なポリシーを学習できることを実証する。
  論文  参考訳（メタデータ） (2021-02-19T10:37:54Z)
• Interpretable Entity Representations through Large-Scale Typing [61.4277527871572]
  本稿では,人間の読みやすいエンティティ表現を作成し,箱から高パフォーマンスを実現する手法を提案する。 我々の表現は、微粒な実体型に対する後続確率に対応するベクトルである。 特定のドメインに対して,学習に基づく方法で,型セットのサイズを縮小できることを示す。
  論文  参考訳（メタデータ） (2020-04-30T23:58:03Z)

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

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