Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “Formal Methods”

Search indexed NASA NTRS and DOE OSTI research on propulsion, heat transfer, battery materials and energy systems. Follow report and document links to the original sources.

Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.

At least 325 records · Page 18
All sourcesNASA NTRSDOE OSTI
NASA NTRSDate not supplied

Formal Specification and Parametric Verification of the ICAROUS Distributed Merging Protocol for Autonomous Aircraft Systems

ICAROUS is a software architecture that provides highly assured core software modules for building safety-centric autonomous unmanned aircraft applications. One of its core components is the ICAROUS distributed merging (IDM) protocol, which allows for decentralized merging of autonomous aircrafts through a designated intersection. This report presents initial results on formal specification and parametric verification of the IDM protocol. We present the development of a formal, discrete-time specification of the ICAROUS distributed merging protocol in TLA+. The developed TLA+ specification includes an abstracted model of the physical aircraft dynamics, the consensus machinery for leader election and coordination, and the computation of merging schedules. In addition, we present details on a command line tool we developed verimerge, that utilizes the TLC model checker for doing bounded, parametric verification and allows for plotting of these results in 2D parameter spaces. The tool also provides functionality for visualization of concrete protocol behaviors, to aid debugging and understanding. We present preliminary, bounded time verification results for a finite number of aircraft. Limitations of the current techniques and possible future extensions of this work are also discussed.

ICAROUS↗
NASA NTRSDate not supplied

Matrix Theory for Data Association in PVS

Consider a collection of data generated by sensors from a set of aircraft. Data association is the process of connecting each sensor measurement with its corresponding aircraft. Furthermore once the data association has taken place, the state of the aircraft can be approximated using a Kalman filter. This talk aims to explore formal specification and verification of data association in the Prototype Verification System (PVS). Formal specification and verification of data association includes development of Kalman filters, Mahalanobis distance, and other topics of matrix analysis in PVS.

Linear Algebra↗
NASA NTRSDate not supplied

A Practical Approach to Uncertainty Quantification Using Probability Boxes

To date, while the use of CFD for aerospace vehicle design and development is prevalent, the documentation of uncertainties associated with the simulations are rare. Instead, the current state-of-the-art relies heavily on the experience of the CFD practitioner to estimate the uncertainty associated with their simulations through simple sensitivity studies or subject matter expertise. This practice will have to be replaced with a formal uncertainty quantification (UQ) process if CFD is to play an expanded role in the research and engineering design community, test and evaluation community, and ultimately certification for flight. Accounting for uncertainties in a formal manner is a tedious process. Moreover, the typical CFD practitioner is not likely to be familiar with formal UQ methods. These factors have prevented the adoption of UQ methods in the engineering design and development cycle. This presentation will outline a credible approach to UQ using Probability Boxes that is straightforward to apply, and can readily be automated using existing UQ tool sets such as the DAKOTA packaged developed at Sandia. The added expense incurred when moving away from a deterministic CFD process to a stochastic one that captures uncertainties to enable risk-informed decision making will be discussed, as well as effective ways to reduce the computational costs.

Uncertainty Quantification↗
NASA NTRS2022

Realizability Checking of Requirements in FRET

Requirements formalization has become increasingly popular in industrial settings as an effort to disambiguate designs and optimize development time and costs for critical system components. Formal requirements elicitation also enables the employment of analysis tools to prove important properties, such as consistency and realizability. In this report, we present the realizability analysis framework that we developed as part of the Formal Requirements Elicitation Tool (FRET). Our framework prioritizes usability, and employs state-of-the-art analysis algorithms that support infinite theories. We demonstrate the workflow for realizability checking, showcase the diagnosis process that supports visualization of conflicts between requirements and simulation of counterexamples, and discuss results from industrial-level case studies.

Formal Requirements Elicitation Tool↗
NASA NTRSDate not supplied

PRECiSA: a static analysis tool for floating-point programs

This presentation introduces PRECiSA, a static analysis framework for analyzing floating-point programs. PRECiSA computes round-off error bounds for a class of floating-point programs, and produces a formal proof certificate of the correctness of these bounds. PRECiSA also has the capability of generating C code which is instrumented to detect unstable branching conditions from a real-number algorithm specification.

Floating-point↗
NASA NTRSDate not supplied

Formal Analysis of the Compact Position Reporting Algorithm

This presentation documents the formal analysis of the compact position reporting (CPR) algorithm. CPR is a fundamental part of Automatic Dependent Surveillance - Broadcast (ADS-B), which is a global protocol for aircraft communication. The formal analysis found and corrected issues with the algorithm, proposed simplifications, and created a formally verified reference implementation, all of which are incorporated in the governing standards document.

Formal Methods↗
NASA NTRSDate not supplied

Embedding Differential Dynamic Logic in PVS

Differential dynamic logic (dL) is a formal framework for specifying and reasoning about hybrid systems, i.e., dynamical systems that exhibit both continuous and discrete behaviors. These kinds of systems arise in many safety- and mission-critical applications. This paper presents a formalization of dL in the Prototype Verification System (PVS) that includes the semantics of hybrid programs and dL’s proof calculus. The formalization embeds dL into the PVS logic, resulting in a version of dL whose proof calculus is not only formally verified, but is also available for the verification of hybrid programs within PVS itself. This embedding, called Plaidypvs (Properly Assured Implementation of dL for Hybrid Program Verification and Specification), supports standard dL style proofs, but further leverages the capabilities of PVS to allow reasoning about entire classes of hybrid programs. The embedding also allows the user to import the well-established definitions and mathematical theories available in PVS.

PVS↗
NASA NTRS2023

Automated Verification of Programmable Logic Controller Programs Against Structured Natural Language Requirements

PLCverif is an actively developed project at CERN, enabling the formal verification of Programmable Logic Controller (PLC) programs in critical systems. In this paper, we present our work on improving the formal requirements specification experience in PLCverif through the use of natural language. To this end, we integrate NASA’s FRET, a formal requirement elicitation and authoring tool, into PLCverif. FRET is used to specify formal requirements in structured natural language, which automatically translates into temporal logic formulae. FRET’s output is then directly used by PLCverif for verification purposes. We discuss practical challenges that PLCverif users face when authoring requirements and the FRET features that help alleviate these problems. We present the new requirement formalization workflow and report our experience using it on two critical CERN case studies.

formal methods↗
NASA NTRSDate not supplied

Formalized Reasoning of Operational Volumes for Wildland Fire Fighting

This work is focused on the formalized reasoning of operational volumes as it relates to the current and future technologies developed by NASA to aid in wildfire fighting operations. One such technology is the unmanned aircraft system pilot kit (UASP-kit) developed by the Scalable Traffic Management for Emergency Response Operations (STEReO) project at NASA, which is used to increase situation awareness for a ground operator in the field. The UASP-kit utilizes operational volumes which represent mission areas and alerting volumes, to alert when another aircraft is within one of these volumes from received ADS-B data. This work is focused on developing a rigorous foundation for the concept of operational volumes for modeling and prototyping operations in such a tool as the UASP-kit. This includes establishing a class of algorithms to detect when an object is in an operational volume, and when an operational volume is intersecting or contained within another. Additionally, this work is focused on providing rigorous proof in an interactive theorem prover that the algorithms work as intended. Scenarios are presented that model current UASP-kit operations and extend past the current capabilities of the technology to modeling more complex scenarios such as mission planning.

Operational Volumes↗
NASA NTRSDate not supplied

Formalized Reasoning of Operational Volumes for Wildland Fire Fighting

This work is focused on the formalized reasoning of operational volumes as it relates to the current and future technologies developed by NASA to aid in wildland firefighting operations. One such technology is the Unmanned Aircraft System Pilot Kit (UASP-kit) developed by the Scalable Traffic Management for Emergency Response Operations (STEReO) project at NASA, which is used to increase situational awareness for a ground operator in the field. The UASP-kit utilizes operational volumes to represent mission areas and alerting volumes; these volumes, in combinations with ADS-B data, can then be used to alert the ground operator when another aircraft has entered one of these areas. This work presents a rigorous foundation for the concept of operational volumes for modeling and prototyping operations in such a tool as the UASP-kit. This includes establishing a class of algorithms to detect when an object is in an operational volume, and when one operational volume intersects or is contained in another. Additionally, this work provides rigorous proof that the algorithms work as intended. Scenarios are presented that model current UASP-kit operations and extend past the current capabilities of the technology to modeling more complex scenarios such as mission planning.

Operational Volumes↗
NASA NTRSDate not supplied

NASA Aeronautics Research Mission Directorate System Security Engineering Approaches

System security engineering (SSE) is a set of formal engineering methods and is considered a subset of systems engineering. It is a relatively new development in systems engineering with the initial NIST (National Institute of Standards) standard published in November of 2016 with updates in 2018, and 2022. The guiding principles in our methodology are based in NIST Special Publication 800-160 Vol. 1 “Systems Security Engineering: Considerations For A Multidisciplinary Approach In The Engineering Of Trustworthy Secure Systems” and integrate methodologies from common IT (Information Technology) threat modeling approaches utilizing MBSE (Model-Based Systems Engineering). The presentation will discuss how our teams utilize SSE and MBSE (Model-Based Systems Engineering) to develop secure architectures for systems under development in our NASA aeronautics research environment. This includes the activities to develop Protection Needs (PN) that, in turn result in security requirements in the design context and policies for the future state operational context for system protection. The process of applying SSE to analyze project architectures and ConOps (Concept of Operations) is intended to ensure the transferred research is both secure and securable in a “real-world” setting.

Systems Security Engineering↗