論文の概要: Varanus: Runtime Verification for CSP

• arxiv url: http://arxiv.org/abs/2506.14426v1
• Date: Tue, 17 Jun 2025 11:42:14 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-18 17:34:59.445296
• Title: Varanus: Runtime Verification for CSP
• Title（参考訳）: Varanus: CSPのランタイム検証
• Authors: Matt Luckcuck, Angelo Ferrando, Fatma Faruq,
• Abstract要約: 本稿では,CSP仕様から構築されたオラクルに対してシステムを監視するRVツールであるVaranusについて述べる。 本ツールは,核廃棄物貯蔵所を検査するロボットローバーを模擬したロボットローバーに適用し,その性能を異なる言語を用いた他の2つのRVツールと実証的に比較する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Autonomous systems are often used in changeable and unknown environments, where traditional verification may not be suitable. Runtime Verification (RV) checks events performed by a system against a formal specification of its intended behaviour, making it highly suitable for ensuring that an autonomous system is obeying its specification at runtime. Communicating Sequential Processes (CSP) is a process algebra usually used in static verification, which captures behaviour as a trace of events, making it useful for RV as well. Further, CSP has more recently been used to specify autonomous and robotic systems. Though CSP is supported by two extant model checkers, so far it has no RV tool. This paper presents Varanus, an RV tool that monitors a system against an oracle built from a CSP specification. This approach enables the reuse without modifications of a specification that was built, e.g during the system's design. We describe the tool, apply it to a simulated autonomous robotic rover inspecting a nuclear waste store, empirically comparing its performance to two other RV tools using different languages, and demonstrate how it can detect violations of the specification. Varanus can synthesise a monitor from a CSP process in roughly linear time, with respect to the number of states and transitions in the model; and checks each event in roughly constant time.
• Abstract（参考訳）: 自律システムはしばしば、従来の検証が適さないような変更可能な未知の環境で使用される。 実行時検証(RV)は、システムが意図した振る舞いの正式な仕様に対して実行するイベントをチェックするため、自律的なシステムが実行時にその仕様に従うことを保証するのに非常に適している。 コミュニケートシーケンスプロセス(Communicating Sequential Processes, CSP)は、静的検証で通常使用されるプロセス代数であり、イベントのトレースとして振る舞いをキャプチャし、RVにも有用である。 さらに、CSPは近年、自律型およびロボットシステムの特定に使われている。 CSPは2つの既存のモデルチェッカーによってサポートされているが、今のところRVツールがない。 本稿では,CSP仕様から構築されたオラクルに対してシステムを監視するRVツールであるVaranusについて述べる。 このアプローチは、例えばシステム設計において、構築された仕様を変更することなく再利用を可能にする。 本稿では,核廃棄物貯蔵庫を検査するロボットローバーを模擬したロボットローバーに適用し,その性能を異なる言語を用いた他の2つのRVツールと実証的に比較し,仕様の違反を検出する方法を示す。 バラヌスは、モデル内の状態と遷移の数に関して、およそ線形時間でCSPプロセスからモニターを合成することができ、各イベントをほぼ一定時間でチェックする。

関連論文リスト

• Querying Perception Streams with Spatial Regular Expressions [3.6814516646862683]
  本研究では空間的および時間的データを含むストリーム上でのパターンマッチングのための新しいクエリ言語としてSpREを紹介する。 我々は、知覚データのためのオフラインおよびオンラインのパターンマッチングフレームワークとしてSTREMツールを開発した。 マッチングフレームワークを使用することで、296ms以内で20,000以上のマッチを見つけることができ、STREMをランタイム監視アプリケーションに適用できます。
  論文  参考訳（メタデータ） (2024-11-08T20:15:27Z)
• Autonomous Vehicle Controllers From End-to-End Differentiable Simulation [60.05963742334746]
  そこで我々は,AVコントローラのトレーニングにAPG(analytic Policy gradients)アプローチを適用可能なシミュレータを提案し,その設計を行う。 提案するフレームワークは, エージェントがより根底的なポリシーを学ぶのを助けるために, 環境力学の勾配を役立てる, エンド・ツー・エンドの訓練ループに, 微分可能シミュレータを組み込む。 ダイナミクスにおけるパフォーマンスとノイズに対する堅牢性の大幅な改善と、全体としてより直感的なヒューマンライクな処理が見られます。
  論文  参考訳（メタデータ） (2024-09-12T11:50:06Z)
• Runtime Verification via Rational Monitor with Imperfect Information [2.7323347531070974]
  従来の検証では完全な情報を前提としており、監視コンポーネントがすべてを正確に認識している。 この仮定は、特に実環境で動作する自律システムでは、しばしば失敗する。 我々は、リニア時間論理特性の標準RVを拡張し、モニターが不完全な情報を持ち、合理的に振る舞うシナリオに対応する。
  論文  参考訳（メタデータ） (2024-08-21T13:56:06Z)
• Generative Modeling of Regular and Irregular Time Series Data via Koopman VAEs [50.25683648762602]
  モデルの新しい設計に基づく新しい生成フレームワークであるKoopman VAEを紹介する。 クープマン理論に触発され、線形写像を用いて潜在条件事前力学を表現する。 KoVAEは、いくつかの挑戦的な合成および実世界の時系列生成ベンチマークにおいて、最先端のGANおよびVAEメソッドより優れている。
  論文  参考訳（メタデータ） (2023-10-04T07:14:43Z)
• Monitoring ROS2: from Requirements to Autonomous Robots [58.720142291102135]
  本稿では,構造化自然言語で記述された要件から自律ロボットのランタイムモニタを生成するための形式的アプローチの概要について述べる。 当社のアプローチでは,Fletal Requirement Elicitation Tool (FRET) とランタイム検証フレームワークであるCopilotを,Ogma統合ツールを通じて統合しています。
  論文  参考訳（メタデータ） (2022-09-28T12:19:13Z)
• On Controller Tuning with Time-Varying Bayesian Optimization [74.57758188038375]
  制御対象とその変更に関する適切な事前知識を用いて、時間変化最適化(TVBO)を用いて、変更環境におけるコントローラのオンラインチューニングを行う。 本研究では,不確実性注入(UI)を用いたTVBO戦略を提案する。 我々のモデルはTVBOの最先端手法よりも優れており、後悔の軽減と不安定なパラメータ構成の低減を実現している。
  論文  参考訳（メタデータ） (2022-07-22T14:54:13Z)
• PSL is Dead. Long Live PSL [3.280253526254703]
  プロパティ仕様言語(英: Property Specification Language、PSL)は、主に独立したドメインで使われている時間論理の一種である。 機械学習技術とPSLモニタを組み合わせることで、PSLを連続的なドメインに拡張できることを示す。
  論文  参考訳（メタデータ） (2022-05-27T17:55:54Z)
• DAE : Discriminatory Auto-Encoder for multivariate time-series anomaly detection in air transportation [68.8204255655161]
  識別オートエンコーダ(DAE)と呼ばれる新しい異常検出モデルを提案する。 通常のLSTMベースのオートエンコーダのベースラインを使用するが、いくつかのデコーダがあり、それぞれ特定の飛行フェーズのデータを取得する。 その結果,DAEは精度と検出速度の両方で良好な結果が得られることがわかった。
  論文  参考訳（メタデータ） (2021-09-08T14:07:55Z)
• SceneChecker: Boosting Scenario Verification using Symmetry Abstractions [3.8995911009078816]
  SceneCheckerは、大きな散らかったワークスペースで複雑な計画を実行する車両のシナリオを検証するツールである。 SceneCheckerは、これらのツールを到達性サブルーチンとして使用しても、検証時間の20倍のスピードアップを示している。
  論文  参考訳（メタデータ） (2020-11-21T03:18:55Z)
• A Framework for Automatic Behavior Generation in Multi-Function Swarms [1.290382979353427]
  マルチファンクションスワムにおける自動行動生成のためのフレームワークを提案する。 フレームワークは3つの同時タスクでシナリオ上でテストされる。 MAP-elitesの挙動特性に及ぼすノイズの影響について検討した。
  論文  参考訳（メタデータ） (2020-07-11T20:50:52Z)

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

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