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

• URL: http://arxiv.org/abs/2501.16274v1
• Date: Mon, 27 Jan 2025 18:06:48 GMT
• Title: What is Formal Verification without Specifications? A Survey on mining LTL Specifications
• Authors: Daniel Neider, Rajarshi Roy,
• Abstract summary: We list and compare 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 formulas, which address different aspects and settings of specification design. We survey the current state-of-the-art techniques and compare them for the convenience of the formal methods practitioners.
• Score: 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.

Related papers

• DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications [59.01527054553122]
  Linear temporal logic (LTL) has recently been adopted as a powerful formalism for specifying complex, temporally extended tasks in reinforcement learning (RL) Existing approaches suffer from several shortcomings: they are often only applicable to finite-horizon fragments, are restricted to suboptimal solutions, and do not adequately handle safety constraints. In this work, we propose a novel learning approach to address these concerns. Our method leverages the structure of B"uchia, which explicitly represent the semantics of automat- specifications, to learn policies conditioned on sequences of truth assignments that lead to satisfying the desired formulae.
  arXiv  Detail & Related papers  (2024-10-06T21:30:38Z)
• SpecGen: Automated Generation of Formal Program Specifications via Large Language Models [20.36964281778921]
  SpecGen is a novel technique for formal program specification generation based on Large Language Models. We evaluate SpecGen on two datasets, including the SV-COMP 279 benchmark and a manually constructed dataset.
  arXiv  Detail & Related papers  (2024-01-16T20:13:50Z)
• Defining and executing temporal constraints for evaluating engineering artifact compliance [56.08728135126139]
  Process compliance focuses on ensuring that the actual engineering work is followed as closely as possible to the described engineering processes. Checking these process constraints is still a daunting task that requires a lot of manual work and delivers feedback to engineers only late in the process. We present an automated constraint checking approach that can incrementally check temporal constraints across inter-related engineering artifacts upon every artifact change.
  arXiv  Detail & Related papers  (2023-12-20T13:26:31Z)
• Natural Language Processing for Requirements Formalization: How to Derive New Approaches? [0.32885740436059047]
  We present and discuss principal ideas and state-of-the-art methodologies from the field of NLP. We discuss two different approaches in detail and highlight the iterative development of rule sets. The presented methods are demonstrated on two industrial use cases from the automotive and railway domains.
  arXiv  Detail & Related papers  (2023-09-23T05:45:19Z)
• Validation-Driven Development [54.50263643323]
  This paper introduces a validation-driven development (VDD) process that prioritizes validating requirements in formal development. The effectiveness of the VDD process is demonstrated through a case study in the aviation industry.
  arXiv  Detail & Related papers  (2023-08-11T09:15:26Z)
• MetricPrompt: Prompting Model as a Relevance Metric for Few-shot Text Classification [65.51149771074944]
  MetricPrompt eases verbalizer design difficulty by reformulating few-shot text classification task into text pair relevance estimation task. We conduct experiments on three widely used text classification datasets across four few-shot settings. Results show that MetricPrompt outperforms manual verbalizer and other automatic verbalizer design methods across all few-shot settings.
  arXiv  Detail & Related papers  (2023-06-15T06:51:35Z)
• Measuring Rule-based LTLf Process Specifications: A Probabilistic Data-driven Approach [2.5407767658470726]
  Declarative process specifications define the behavior of processes by means of rules based on Linear Temporal Logic on Finite Traces. In a mining context, these specifications are inferred from, and checked on, multi-sets of runs recorded by information systems. We propose a technique that measures the degree of satisfaction of specifications over event logs.
  arXiv  Detail & Related papers  (2023-05-09T13:07:01Z)
• Specification sketching for Linear Temporal Logic [3.3946853660795893]
  We propose a fundamentally novel approach to writing formal specifications, named specification sketching for Linear Temporal Logic (LTL) The key idea is that an engineer can provide a partial formula, called a sketch, where parts that are hard to formalize can be left out. We show that deciding whether a sketch can be completed falls into the complexity class NP and present two SAT-based sketching algorithms.
  arXiv  Detail & Related papers  (2022-06-14T10:09:23Z)
• From English to Signal Temporal Logic [7.6398837478968025]
  We propose DeepSTL, a tool and technique for the translation of informal requirements, given as free English sentences, into Signal Temporal Logic (STL), a formal specification language for cyber-physical systems. A major challenge to devise such a translator is the lack of publicly available informal requirements and formal specifications. In the second step, we use a state-of-the-art transformer-based neural translation technique, to train an accurate attentional translator of English to STL.
  arXiv  Detail & Related papers  (2021-09-21T16:13:29Z)
• A Diagnostic Study of Explainability Techniques for Text Classification [52.879658637466605]
  We develop a list of diagnostic properties for evaluating existing explainability techniques. We compare the saliency scores assigned by the explainability techniques with human annotations of salient input regions to find relations between a model's performance and the agreement of its rationales with human ones.
  arXiv  Detail & Related papers  (2020-09-25T12:01:53Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  We propose a model-free RL algorithm that enables the use of Linear Temporal Logic (LTL) to formulate a goal for unknown continuous-state/action Markov Decision Processes (MDPs) The algorithm is guaranteed to synthesise a control policy whose traces satisfy the specification with maximal probability.
  arXiv  Detail & Related papers  (2019-02-02T20:09:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.