論文の概要: Trace-Based Execution-Level Observability of VDM-SL Specifications
- arxiv url: http://arxiv.org/abs/2608.19510v1
- Date: Thu, 20 Aug 2026 00:02:38 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-21 20:28:51.418003
- Title: Trace-Based Execution-Level Observability of VDM-SL Specifications
- Title(参考訳): VDM-SL仕様のトレースベース実行レベル可観測性
- Abstract要約: VDMは、数学的定理証明とシミュレーション実行によるソフトウェアテストを通じて厳密な検証を追求してきた。
デバッガでのステップバイステップ実行では、ユーザが操作の内部動作に従うこともできる。
本稿では,操作の内部動作を永続的かつ解析可能にするために,代入や操作呼び出し,返却文の実行トレースの記録と利用を提案する。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: VDM has been pursuing rigorous verification through mathematical theorem proving and software testing via simulated execution. Animation through an interpreter enables validation of the specification to ensure it meets the required functionality. Step-by-step execution in a debugger also allows the user to follow the internal behavior of operations. In this paper, we propose the recording and utilization of execution traces of assignments, operation calls, and return statements to make the internal behavior of operations persistent and analyzable as state-based models. The data model of events in execution traces, its implementation in ViennaTalk, and its application to visualization will be introduced.
- Abstract(参考訳): VDMは、数学的定理証明とシミュレーション実行によるソフトウェアテストを通じて厳密な検証を追求してきた。
インタプリタによるアニメーションにより、仕様の検証が可能になり、必要な機能を満たすことができる。
デバッガでのステップバイステップ実行では、ユーザが操作の内部動作に従うこともできる。
本稿では、状態ベースモデルとして操作の内部動作を永続的かつ解析可能にするために、代入、操作呼び出し、返却文の実行トレースの記録と利用を提案する。
実行トレース中のイベントのデータモデル、ウィーンTalkにおける実装、可視化への応用を紹介する。
関連論文リスト
- ETAS: An Effect-Typed Language for Agent Systems [3.1440390119576676]
ETASはエージェントシステムのためのプログラミング言語である。
モデル支援エージェント、ツールコール、プロンプト、型付きメモリ、人間の承認、ポリシー、実行トレースをセマンティックプログラム要素として扱う。
論文 参考訳(メタデータ) (2026-07-20T10:11:53Z) - PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
我々は、スケジューリング、検証、メモリ、ベンチマーク、安全性をシステムレベルのサービスとして提供するPhyAgentOSを紹介します。
セッション中心のセッションは、スケジューリング、互換性、監督された実行、エビデンス収集、受け入れの最小単位として、アクションではなくセッションを扱う。
SessionVerifierは、実行終了とセマンティックタスク完了を、成功、失敗、または再計画のエビデンスに基づいて判断する。
ベンチマークはデプロイメントセッションと検証パスを再利用するので、結果は実際の実行に遡る。
論文 参考訳(メタデータ) (2026-07-18T04:46:53Z) - RoboProcessBench: Benchmarking Process-Aware Understanding in Vision-Language Robotic Manipulation [59.10505906182782]
視覚言語モデル(VLM)は、ロボット操作における視覚的批判、報酬発生器、障害検出器として、ますます研究されている。
既存の評価では、VLMが微細なプロセス理解を持っているかどうかを検証できない。
本稿では、視覚言語ロボット操作におけるプロセス認識理解のベンチマークであるRoboProcessBenchを紹介する。
論文 参考訳(メタデータ) (2026-06-11T08:20:42Z) - From Abstraction to Instantiation: Learning Behavioral Representation for Vision-Language-Action Model [76.88595728131288]
VLA(Vision-Language-Action)モデルは、分散シフト時にしばしば性能劣化に悩まされる。
時間的コヒーレントな行動表現の学習を通じて堅牢な操作を容易にするフレームワークである textbfBehaviorVLA を提案する。
RoboTwin 2.0、LIBERO、CALVINの実験では、最先端の成功率は58%、98%、および4.36(Avg.Len)である。
論文 参考訳(メタデータ) (2026-05-21T16:14:19Z) - Monitoring Data-aware Temporal Properties (Extended Version) [56.386411908764494]
有限トレース上の任意のSMT理論に富む線形時間特性の予測モニタリングについて考察する。
この設定での予測モニタリングは非常に困難であり、監視状態はこれまでのトレースプレフィックスと可能な有限継続の両方に依存している。
本研究は,表現的フラグメントオフMTにおける特性モニタリングのための新しい基礎的枠組みの正しさを提示し,正式に証明するものである。
論文 参考訳(メタデータ) (2026-05-14T10:23:11Z) - Modeling and Simulation Based Engineering in the Context of Cyber-Physical Systems [51.82266520875928]
実行セマンティクスは、第一級のエンジニアリングエンティティとして扱われない。
モデリングとシミュレーションに基づくエンジニアリングは、正式な実行、実験的な実行、検証、アクティビティによる検証を交互に行う反復サイクルのエンジニアリングを組織する。
これらの応用は、フレームワークがCPSを超えて、明示的に定義された実行条件に依存するあらゆるシステムに一般化することを示している。
論文 参考訳(メタデータ) (2026-04-13T12:42:12Z) - A Physical Agentic Loop for Language-Guided Grasping with Execution-State Monitoring [5.437966695589128]
我々は、接地された実行状態上で動作する有界な実施エージェントとして言語誘導の把握を再構築する。
未修正の学習操作プリミティブをラップする物理エージェントループを導入する。
眼内カメラD405を用いた移動マニピュレータのループを検証した。
論文 参考訳(メタデータ) (2026-04-08T08:01:35Z) - Self-Execution Simulation Improves Coding Models [37.139165988182654]
プログラム実行をステップバイステップでシミュレートするために、Code LLMをトレーニングできることを示します。
提案手法は、自然言語実行トレースの教師付き微調整と、真の実行に基づくテキスト説明と強化学習を組み合わせたものである。
論文 参考訳(メタデータ) (2026-03-11T15:28:22Z) - Explanatory Model Monitoring to Understand the Effects of Feature Shifts on Performance [61.06245197347139]
そこで本研究では,機能シフトによるブラックボックスモデルの振る舞いを説明する新しい手法を提案する。
本稿では,最適輸送と共有値の概念を組み合わせた提案手法について,説明的性能推定として紹介する。
論文 参考訳(メタデータ) (2024-08-24T18:28:19Z) - Sound Concurrent Traces for Online Monitoring Technical Report [0.0]
並列プログラムは通常、抽象的なプログラム実行のためのトレースの収集に依存します。
まず、トレースが並列実行を表すときの概念を定義します。
次に,非ブロッキングベクトルクロックアルゴリズムを提案し,音の同時トレースをハエで収集する。
論文 参考訳(メタデータ) (2024-02-28T15:11:39Z) - Outcome-Oriented Prescriptive Process Monitoring Based on Temporal Logic
Patterns [9.876717580544364]
本稿では,新しいアウトカム指向の規範的プロセスモニタリングシステムを提案する。
プロセス実行中に保証されるアクティビティ間の時間的関係を推奨します。
これにより、特定の時点におけるアクティビティの強制実行が緩和されるため、ユーザによる自由度が向上する。
論文 参考訳(メタデータ) (2022-11-09T13:36:07Z) - Chain of Thought Imitation with Procedure Cloning [129.62135987416164]
本稿では,一連の専門家計算を模倣するために,教師付きシーケンス予測を適用したプロシージャクローニングを提案する。
本研究では、専門家の行動の中間計算を模倣することで、プロシージャのクローン化により、未知の環境構成に顕著な一般化を示すポリシーを学習できることを示す。
論文 参考訳(メタデータ) (2022-05-22T13:14:09Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。