Automated Formalization of Probabilistic Requirements from Structured Natural Language

TL;DR

This paper tackles the difficulty of expressing probabilistic requirements for autonomous, safety-critical systems by extending NASA's FRETish structured natural language with a probabilistic field and holding-condition support. It introduces a compositional translation to $PCTL^*$, backed by SALT-based path formula generation and a formal validation framework that uses DTMCs and PRISM to ensure semantic fidelity. The approach dramatically increases expressiveness (to 560 template keys) and demonstrates strong practical utility through both literature-based and industrial case studies, capturing the majority of probabilistic requirements and enabling automated formal analysis. The work also discusses usability, integration with existing tooling, and the role of structured natural language in bridging human-readable requirements with formal specifications, while outlining future enhancements for nested patterns and broader logics.

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.

Figures (6)

• Figure 1: Probabilistic FRET: extensions to classic FRET components are shown with dashed lines; new components are highlighted with solid lines and a colored background.
• Figure 2: FRET's probabilistic requirement editor. On the left, the requirement is entered in FRETish. The initial, unstructured natural language version of the requirement (pure English) is entered in the Comments field. On the right, FRET provides an explanation of the requirement semantics and the generated PCTL* formula.
• Figure 3: An example of a generated DTMC used for validation. States are defined by a 5-tuple ($t,m,c,sc,r$) representing time, mode, cond, stop and res. The first element, $t$, tracks time by counting transitions from the initial state. The other four elements are boolean indicators for mode ($m$), cond ($c$), stop ($sc$), and res ($r$), where 1 signifies that the proposition is true in that state and 0 signifies it is false.
• Figure 4: Simplified RTRC-provisioned perception system overview. This system generates an estimate, $\hat{q}$, of $q$ at time $k$. Multiple sensors (traditional and LEC) collect data that are then processed by a series of estimators. The LEC components can be enhanced with out-of-distribution (OOD) detectors, which set a flag $f_k$ when an OOD value is predicted. A sensor selector combines these estimates to produce a single estimate, $\hat{q}_k$.
• Figure 5: The total number of occurrences for each template key per requirement set.

Theorems & Definitions (2)

• Theorem 1
• proof