論文の概要: What is Formal Verification without Specifications? A Survey on mining LTL Specifications
- arxiv url: http://arxiv.org/abs/2501.16274v1
- Date: Mon, 27 Jan 2025 18:06:48 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-01-28 13:54:25.334184
- Title: What is Formal Verification without Specifications? A Survey on mining LTL Specifications
- Title（参考訳）: 仕様のない形式的検証とは何か? LTL仕様のマイニングに関する調査
- Authors: Daniel Neider, Rajarshi Roy,
- Abstract要約: リアクティブシステムのためのデファクト標準仕様言語であるLTL(Linear Temporal Logic)のマイニング仕様の進歩をリストし比較する。
いくつかのアプローチは、仕様設計の異なる側面と設定に対処する公式を学習するために設計されている。
本研究は,現在の最先端技術について調査し,形式的手法実践者の利便性について比較する。
- 参考スコア（独自算出の注目度）: 5.655251163654288
- License:
- Abstract: Virtually all verification techniques using formal methods rely on the availability of a formal specification, which describes the design requirements precisely. However, formulating specifications remains a manual task that is notoriously challenging and error-prone. To address this bottleneck in formal verification, recent research has thus focussed on automatically generating specifications for formal verification from examples of (desired and undesired) system behavior. In this survey, we list and compare recent advances in mining specifications in Linear Temporal Logic (LTL), the de facto standard specification language for reactive systems. Several approaches have been designed for learning LTL formulas, which address different aspects and settings of specification design. Moreover, the approaches rely on a diverse range of techniques such as constraint solving, neural network training, enumerative search, etc. We survey the current state-of-the-art techniques and compare them for the convenience of the formal methods practitioners.
- Abstract（参考訳）: 形式的手法を用いた検証手法は、設計要件を正確に記述した形式的仕様の可用性に依存している。
しかし、仕様書の定式化は依然として手作業であり、非常に困難でエラーを起こしやすい。
フォーマルな検証におけるこのボトルネックに対処するため、最近の研究は(望ましくない)システム動作の例から、フォーマルな検証のための仕様を自動生成することに重点を置いている。
本稿では、リアクティブシステムのためのデファクト標準仕様言語であるLTL(Linear Temporal Logic)のマイニング仕様の最近の進歩をリストし、比較する。
仕様設計の異なる側面と設定に対処するLTL式を学習するために、いくつかのアプローチが設計されている。
さらに、アプローチは制約解決、ニューラルネットワークトレーニング、列挙型検索など、さまざまなテクニックに依存しています。
本研究は,現在の最先端技術について調査し,形式的手法実践者の利便性について比較する。
関連論文リスト
- DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications [59.01527054553122]
リニア時間論理(LTL)は、強化学習(RL)における複雑で時間的に拡張されたタスクを特定する強力なフォーマリズムとして最近採用されている。
既存のアプローチはいくつかの欠点に悩まされており、それらは有限水平フラグメントにのみ適用でき、最適以下の解に制限され、安全制約を適切に扱えない。
本研究では,これらの問題に対処するための新しい学習手法を提案する。
提案手法は, 自動仕様のセマンティクスを明示的に表現したB"uchiaの構造を利用して, 所望の式を満たすための真理代入の順序を条件としたポリシーを学習する。
論文 参考訳（メタデータ） (2024-10-06T21:30:38Z) - SpecGen: Automated Generation of Formal Program Specifications via Large Language Models [20.36964281778921]
SpecGenは、大規模言語モデルに基づく形式的なプログラム仕様生成のための新しいテクニックである。
SV-COMP 279ベンチマークと手動で構築したデータセットを含む2つのデータセット上でSpecGenを評価する。
論文 参考訳（メタデータ） (2024-01-16T20:13:50Z) - Defining and executing temporal constraints for evaluating engineering
artifact compliance [56.08728135126139]
プロセスコンプライアンスは、実際のエンジニアリング作業が記述されたエンジニアリングプロセスに可能な限り密接に従うことを保証することに焦点を当てます。
これらのプロセスの制約をチェックすることは、依然として大変な作業であり、多くの手作業を必要とし、プロセスの後半にエンジニアにフィードバックを提供する。
関連するエンジニアリングアーティファクト間の時間的制約を,アーティファクトの変更毎に段階的にチェックする,自動制約チェックアプローチを提案する。
論文 参考訳（メタデータ） (2023-12-20T13:26:31Z) - Natural Language Processing for Requirements Formalization: How to
Derive New Approaches? [0.32885740436059047]
我々はNLPの分野における主要な考え方と最先端の方法論について論じる。
我々は2つの異なるアプローチを詳細に議論し、ルールセットの反復的開発を強調した。
提案手法は, 自動車分野と鉄道分野の2つの産業分野において実証された。
論文 参考訳（メタデータ） (2023-09-23T05:45:19Z) - Validation-Driven Development [54.50263643323]
本稿では,形式的開発における要件の検証を優先する検証駆動開発(VDD)プロセスを紹介する。
VDDプロセスの有効性は、航空業界におけるケーススタディを通じて実証されている。
論文 参考訳（メタデータ） (2023-08-11T09:15:26Z) - MetricPrompt: Prompting Model as a Relevance Metric for Few-shot Text
Classification [65.51149771074944]
MetricPromptは、数発のテキスト分類タスクをテキストペア関連性推定タスクに書き換えることで、言語設計の難易度を緩和する。
広範に使われている3つのテキスト分類データセットを4つのショット・セッティングで実験する。
結果から,MetricPromptは,手動弁証法や自動弁証法よりも優れた性能を示した。
論文 参考訳（メタデータ） (2023-06-15T06:51:35Z) - Measuring Rule-based LTLf Process Specifications: A Probabilistic
Data-driven Approach [2.5407767658470726]
宣言的プロセス仕様は、有限トレース上の線形時間論理に基づくルールによってプロセスの振舞いを定義します。
マイニングの文脈では、これらの仕様は情報システムによって記録された複数セットの実行から推論され、チェックされる。
本稿では,イベントログに対する仕様書の満足度を測定する手法を提案する。
論文 参考訳（メタデータ） (2023-05-09T13:07:01Z) - Specification sketching for Linear Temporal Logic [3.3946853660795893]
線形時相論理(LTL)のための仕様スケッチという,形式仕様を書くための基本的新しいアプローチを提案する。
鍵となるアイデアは、エンジニアがスケッチと呼ばれる部分的な公式を提供することができることだ。
そこで本研究では,スケッチが完成するかどうかを複雑性クラスNPに分類し,SATベースのスケッチアルゴリズムを2つ提示する。
論文 参考訳（メタデータ） (2022-06-14T10:09:23Z) - From English to Signal Temporal Logic [7.6398837478968025]
本稿では,サイバー物理システムのための公式な仕様言語であるSignal Temporal Logic (STL) に,自由英語文として与えられる非公式な要件を翻訳するためのツールおよびテクニックであるDeepSTLを提案する。
このような翻訳を考案する上での大きな課題は、公式な非公式な要件と公式な仕様の欠如である。
2番目のステップでは、最先端のトランスフォーマーベースのニューラル翻訳技術を用いて、英語からSTLへの正確な注意翻訳を訓練する。
論文 参考訳（メタデータ） (2021-09-21T16:13:29Z) - A Diagnostic Study of Explainability Techniques for Text Classification [52.879658637466605]
既存の説明可能性技術を評価するための診断特性のリストを作成する。
そこで本研究では, モデルの性能と有理性との整合性の関係を明らかにするために, 説明可能性手法によって割り当てられた有理性スコアと有理性入力領域の人間のアノテーションを比較した。
論文 参考訳（メタデータ） (2020-09-25T12:01:53Z) - Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。
このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
論文 参考訳（メタデータ） (2019-02-02T20:09:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。