What is formal verification without specifications? A survey on mining LTL specifications
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 f...
| Päätekijät: | , |
|---|---|
| Aineistotyyppi: | Book section |
| Kieli: | English |
| Julkaistu: |
Springer
2024
|
| _version_ | 1826316838065143808 |
|---|---|
| author | Neider, D Roy, R |
| author_facet | Neider, D Roy, R |
| author_sort | Neider, D |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-12-09T03:26:52Z |
| format | Book section |
| id | oxford-uuid:e9cbc9c7-9740-4f1c-a3f0-d5beb592f9fd |
| institution | University of Oxford |
| language | English |
| last_indexed | 2025-02-19T04:30:47Z |
| publishDate | 2024 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:e9cbc9c7-9740-4f1c-a3f0-d5beb592f9fd2024-12-16T11:27:12ZWhat is formal verification without specifications? A survey on mining LTL specificationsBook sectionhttp://purl.org/coar/resource_type/c_3248uuid:e9cbc9c7-9740-4f1c-a3f0-d5beb592f9fdEnglishSymplectic ElementsSpringer2024Neider, DRoy, RVirtually 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. |
| spellingShingle | Neider, D Roy, R What is formal verification without specifications? A survey on mining LTL specifications |
| title | What is formal verification without specifications? A survey on mining LTL specifications |
| title_full | What is formal verification without specifications? A survey on mining LTL specifications |
| title_fullStr | What is formal verification without specifications? A survey on mining LTL specifications |
| title_full_unstemmed | What is formal verification without specifications? A survey on mining LTL specifications |
| title_short | What is formal verification without specifications? A survey on mining LTL specifications |
| title_sort | what is formal verification without specifications a survey on mining ltl specifications |
| work_keys_str_mv | AT neiderd whatisformalverificationwithoutspecificationsasurveyonminingltlspecifications AT royr whatisformalverificationwithoutspecificationsasurveyonminingltlspecifications |