Natural Language Processing based Auto Generation of Proof Obligations for Formal Verification of Control Requirements in Safety-Critical Systems

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F25%3A7236UBCR" target="_blank" >RIV/00216208:11320/25:7236UBCR - isvavai.cz</a>

Result on the web

<a href="https://www.scopus.com/inward/record.uri?eid=2-s2.0-85195441708&doi=10.1016%2fj.ifacol.2024.05.001&partnerID=40&md5=cd9a9f04d07ef5c860ce10852a78ea52" target="_blank" >https://www.scopus.com/inward/record.uri?eid=2-s2.0-85195441708&doi=10.1016%2fj.ifacol.2024.05.001&partnerID=40&md5=cd9a9f04d07ef5c860ce10852a78ea52</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1016/j.ifacol.2024.05.001" target="_blank" >10.1016/j.ifacol.2024.05.001</a>

Result language

angličtina

Original language name

Natural Language Processing based Auto Generation of Proof Obligations for Formal Verification of Control Requirements in Safety-Critical Systems

Original language description

Formal verification uses mathematically rigorous techniques to establish the correctness of an algorithm or model. While traditional testing shows the presence of defects, it cannot guarantee the absence of defects in a design. Formal verification, on the other hand, can guarantee the absence of defects concerning a set of desirable properties, or provide counter-examples where the properties do not hold. Despite its value, it is not commonly used due to various reasons. This paper discusses two major reasons and proposes solutions for them. The first reason is the difficulty in deriving the proof obligations, the properties to be proved, from the textual requirements. The second hindrance is the additional effort in developing the infrastructure for formal verification. The paper proposes a Natural Language Processing (NLP) based approach to automatically suggest the proof obligations from the textual requirements to remove the first hindrance. They are expressed in propositional, Linear-time Temporal Logic (LTL), and a few customized expressions. The paper also provides methods for converting these obligations into verification subsystems which enable model checking, a method of formal verification to be invoked on the design model, thereby alleviating the second hindrance. The approach and methods are explained in the context of a flight control system's fault handling and safety requirements. © 2024 The Authors.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

—

Continuities

—

Publication year

2024

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

IFAC-PapersOnLine

ISBN

—

ISSN

2405-8963

e-ISSN

—

Number of pages

6

Pages from-to

43-48

Publisher name

Elsevier B.V.

Place of publication

—

Event location

Delhi

Event date

Jan 1, 2025

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—