Automated Formalization of Probabilistic Requirements from Structured Natural Language

TL;DR

This paper introduces an extension to a natural language tool that automatically translates structured probabilistic requirements into formal logic, facilitating analysis of safety-critical autonomous systems.

Contribution

It extends NASA's FRET tool to support probabilistic requirements and automates their translation into formal logic with validation and proof mechanisms.

Findings

Automated translation from structured natural language to probabilistic logic.

Validation framework ensures correctness and well-formedness.

Enhanced tool usability for developers in safety-critical domains.

Abstract

Integrating autonomous and adaptive behavior into software-intensive systems presents significant challenges for software development, as uncertainties in the environment or decision-making processes must be explicitly captured. These challenges are amplified in safety- and mission-critical systems, which must undergo rigorous scrutiny during design and development. Key among these challenges is the difficulty of specifying requirements that use probabilistic constructs to capture the uncertainty affecting these systems. To enable formal analysis, such requirements must be expressed in precise mathematical notations such as probabilistic logics. However, expecting developers to write requirements directly in complex formalisms is unrealistic and highly error-prone. We extend the structured natural language used by NASA's Formal Requirement Elicitation Tool (FRET) with support for the specification of unambiguous and correct probabilistic requirements, and develop an automated approach for translating these requirements into logical formulas. We propose and develop a formal, compositional, and automated approach for translating structured natural-language requirements into formulas in probabilistic temporal logic. To increase trust in our formalizations, we provide assurance that the generated formulas are well-formed and conform to the intended semantics through an automated validation framework and a formal proof. The extended FRET tool enables developers to specify probabilistic requirements in structured natural language, and to automatically translate them into probabilistic temporal logic, making the formal analysis of autonomous and adaptive systems more practical and less error-prone.