What is Formal Verification without Specifications? A Survey on mining LTL Specifications

要約

正式な方法を使用した実質的にすべての検証手法は、設計要件を正確に説明する正式な仕様の可用性に依存しています。
ただし、仕様の策定は、悪名高い挑戦的でエラーが発生しやすいマニュアルタスクのままです。
このボトルネックに正式な検証で対処するために、最近の研究は、（望ましい）システムの動作の例から正式な検証のための仕様を自動的に生成することに焦点を当てています。
この調査では、リアクティブシステムの事実上の標準仕様言語である線形時間論的論理（LTL）のマイニング仕様の最近の進歩をリストと比較します。
仕様設計のさまざまな側面と設定に対処するLTL式を学習するために、いくつかのアプローチが設計されています。
さらに、このアプローチは、制約解決、ニューラルネットワークトレーニング、列挙検索などの多様な技術に依存しています。現在の最新技術を調査し、正式な方法実務家の便利さについてそれらを比較します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google