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

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

—

Návaznosti

—

Rok uplatnění

2024

Kód důvěrnosti údajů

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

Název statě ve sborníku

IFAC-PapersOnLine

ISBN

—

ISSN

2405-8963

e-ISSN

—

Počet stran výsledku

6

Strana od-do

43-48

Název nakladatele

Elsevier B.V.

Místo vydání

—

Místo konání akce

Delhi

Datum konání akce

1. 1. 2025

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—