Engineering Papers⌕ Search

Engineering topics

Paolo Masci

Publications and source records attributed to Paolo Masci.

16 records
All sourcesNASA NTRSDOE OSTI
NASA NTRS2022

Towards an Implementation of Differential Dynamic Logic in PVS

This paper describes an ongoing effort to embed and verify differential dynamic logic (dL) in the Prototype Verification System (PVS). dL is a logic for specifying and formally reasoning about hybrid systems, which employ both continuous and discrete dynamics. There are several benefits of this effort. First, the embedding of dL in PVS offers an independent formal verification of the semantics and rules of dL. Second, the embedding is fully operational within PVS, giving PVS practitioners the ability to use dL in the formal specification and verification process. Third, the rich specification language, type system, and powerful interactive prover of PVS can be used on dL objects. In addition to the embedding and verification of dL, a custom extension for Visual Studio Code has been developed, so that a stylized dL syntax can be used to specify hybrid programs and their properties.

Differential Dynamic Logic↗
NASA NTRSDate not supplied

An Integrated Development Environment for the Prototype Verification System

The steep learning curve of formal technologies is a well-known barrier to the adoption of formal verification tools in industry. This paper presents VSCode-PVS, a modern integrated development environment for the Prototype Verification System (PVS). This new environment integrates the editing and proof management functionalities of PVS in Visual Studio Code, a popular code editor widely used by software developers. VSCode-PVS provides functionalities that developers expect to find in modern verification tools but are not available in the standard Emacs front-end of PVS, such as auto-completion, point-and-click navigation of definitions, live diagnostics for errors, and literate programming. The main features and architecture of the environment are presented, along with a comparison with other similar tools.

Paolo Masci↗
NASA NTRSDate not supplied

Proof Mate: An Interactive Proof Helper for PVS (Tool Paper)

This paper presents Proof Mate, an interactive proof helper for the PVS verification system. The helper is integrated in VSCode-PVS, the Visual Studio Code extension for PVS. It extends the capabilities of VSCode-PVS by introducing new functionalities for suggesting proof commands, sketching proof attempts, and repairing broken proofs during interactive proof sessions. This work further aligns VSCode-PVS to the functionalities provided by modern development tools, with the ultimate aim to facilitate the adoption of formal methods in engineering practices and education.

Interactive Theorem Proving↗
NASA NTRSDate not supplied

Proof Mate: An Interactive Proof Helper for PVS

This paper presents Proof Mate, an interactive proof helper for the PVS verification system. The helper is integrated in VSCode-PVS, the Visual Studio Code extension for PVS. It extends the capabilities of VSCode-PVS by introducing new functionalities for suggesting proof commands, sketching proof attempts, and repairing broken proofs during interactive proof sessions. This work further aligns VSCode-PVS to the functionalities provided by modern development tools, with the ultimate aim to facilitate the adoption of formal methods in engineering practices and education.

Formal Methods↗
NASA NTRSDate not supplied

Assistive Detect and Avoid for Pilots in the Cockpit

Aircraft not receiving radar services rely on see and avoid and radio coordination via Common Traffic Advisory Frequencies to remain well clear of each other and avoid mid-air collisions. Radio coordination is usually performed in the vicinity of non-towered airports whereas non-radar services en-route operations rely solely on see and avoid. This paper presents the results of a simulation study of the effectiveness of assistive detect and avoid technologies when used to enhance pilots’ ability to see and avoid nearby traffic. Three different experimental conditions are modeled, representing “unaided see and avoid”, “see and avoid with traffic advisories”, and “see and avoid with assistive detect and avoid technology”. The effectiveness of see and avoid is evaluated using a set of head-on, crossing, and overtaking encounter scenarios and a model of visual acquisition embedded in a Monte Carlo simulation. The effectiveness of assistive detect and avoid is estimated for the same encounter scenarios. A prototype system for detect and avoid and a summary of results are presented. Preliminary results strongly suggest that assistive detect and avoid could greatly enhance the capabilities of flight crews to avoid traffic and remain well clear.

collision, detect and avoid, resolution, well clea↗
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

DANTi, DAA in the Cockpit

DANTi is a prototype Electronic Flight Bag which incorporates an assistive Detect and Avoid (DAA) capability developed by NASA.

Maria Consiglio↗
NASA NTRSDate not supplied

Assistive Detect and Avoid for Pilots in the Cockpit

Aircraft not receiving radar services rely on see and avoid and radio coordination via Common Traffic Advisory Frequencies to remain well clear of each other and avoid mid-air collisions. Radio coordination is usually performed in the vicinity of non-towered airports whereas non-radar services en-route operations rely solely on see and avoid. This paper presents the results of a simulation study of the effectiveness of assistive detect and avoid technologies when used to enhance pilots’ ability to see and avoid nearby traffic. Three different experimental conditions are modeled, representing “unaided see and avoid”, “see and avoid with traffic advisories”, and “see and avoid with assistive detect and avoid technology”. The effectiveness of see and avoid is evaluated using a set of head-on, crossing, and overtaking encounter scenarios and a model of visual acquisition embedded in a Monte Carlo simulation. The effectiveness of assistive detect and avoid is estimated for the same encounter scenarios. A prototype system for detect and avoid and a summary of results are presented. Preliminary results strongly suggest that assistive detect and avoid could greatly enhance the capabilities of flight crews to avoid traffic and remain well clear.

collision↗
NASA NTRSDate not supplied

Interpretation and Formalization of the Right-of-Way Rules

This paper presents an interpretation and mathematical definition of the right-of-way rules as stated in USA, Title 14 of the Code of Federal Regulations, Part 91, Section 91.113 (14 CFR 91.113). In an encounter between two aircraft, the right-of-way rules defines which aircraft, if any, has the right-of-way and which AQ2 aircraft must maneuver to stay well clear of the other aircraft. The objective of the work presented in this paper is to give an unambiguous interpretation of the rules. From the interpretation, a precise mathematical formulation is created that can be used for analysis and proof of properties. The mathematical formulation has been defined in the Prototype Verification System (PVS) and properties of well formedness and core properties of the formalization have been mechanically proved. This mathematical formulation can be implemented digitally, so that right-of-way rules can be used in simulation or in future autonomous operations.

Right-of-Way↗
NASA NTRSDate not supplied

DANTi: A Tool for Assistive Detect and Avoid Research

This paper presents DANTi, a research tool developed at NASA Langley Research Center to support the validation of Assistive Detect and Avoid (ADAA) requirements for General Aviation (GA). ADAA is a future on-board aircraft technology intended to augment a pilot’s see-and-avoid capability by helping them identify and resolve traffic conflicts earlier and more efficiently. DANTi includes a realistic Electronic Flight Bag (EFB) display and a fast-time simulation environment that can be fully customized to meet different research requirements. DANTi is currently used within NASA efforts such as the Air Mobility Pathfinders project on future air transportation systems and a joint NASA/FAA Laboratory Integrated Test Environment (NFLITE) on next-generation airspace operations in urban environments. These efforts investigate ADAA requirements in advanced urban air mobility settings where new aircraft types, new services, and new traffic patterns will be integrated in an overall crowded airspace.

Detect and Avoid↗
NASA NTRSDate not supplied

Assistive Detect and Avoid Technology in Urban Air Mobility Environments

The use of Assistive Detect and Avoid (Assistive DAA or ADAA) technology in Urban Air Mobility (UAM) environments poses potential benefits as well as challenges. Assistive DAA refers to the leveraged use of DAA technology, originally developed to replace see-and-avoid capabilities for remotely piloted aircraft, in onboard-piloted aircraft to augment (rather than replace) pilots’ see-and-avoid abilities and thus enhance the safety and efficiency of visual flight operations. ADAA is anticipated to be especially safety-enhancing in airspace where traffic density is high or traditional air traffic services are limited, such as in future UAM environments. ADAA may also enable higher-tempo UAM operations than with only see-and-avoid capabilities, while still maintaining acceptable levels of safety. UAM concepts under development by the FAA, NASA, and industry focus on operations moving people and cargo in urban and suburban areas using innovative technologies, operations, and aircraft, including electric vertical takeoff and landing (eVTOL) aircraft. Researchers at NASA Langley Research Center, in collaboration with FAA researchers at the William J. Hughes Technical Center in Atlantic City, NJ, have conducted a series of medium-fidelity, human-in-the-loop research simulations of potential future UAM operations and concepts in both Class C and Class B airspace environments. These simulations have included use of a Langley-developed ADAA research tool called DANTi, which enables configurable ADAA displays to be presented to pilots of simulated eVTOL aircraft participating in higher-density and higher-tempo UAM operations. Experience and observations made during testing of the NASA-developed DANTi ADAA capability in the UAM NFLITE simulation environment will be reported in this paper together with a discussion of airspace integration and regulatory topics.

Detect and Avoid↗
NASA NTRSDate not supplied

Assistive Detect and Avoid Technology in Urban Air Mobility Environments

The use of Assistive Detect and Avoid (Assistive DAA or ADAA) technology in Urban Air Mobility (UAM) environments poses potential benefits as well as challenges. Assistive DAA refers to the leveraged use of DAA technology, originally developed to replace see-and-avoid capabilities for remotely piloted aircraft, in onboard-piloted aircraft to augment (rather than replace) pilots’ see-and-avoid abilities and thus enhance the safety and efficiency of visual flight operations. ADAA is anticipated to be especially safety-enhancing in airspace where traffic density is high or traditional air traffic services are limited, such as in future UAM environments. ADAA may also enable higher-tempo UAM operations than with only see-and-avoid capabilities, while still maintaining acceptable levels of safety. UAM concepts under development by the FAA, NASA, and industry focus on operations moving people and cargo in urban and suburban areas using innovative technologies, operations, and aircraft, including electric vertical takeoff and landing (eVTOL) aircraft. Researchers at NASA Langley Research Center, in collaboration with FAA researchers at the William J. Hughes Technical Center in Atlantic City, NJ, have conducted a series of medium-fidelity, human-in-the-loop research simulations of potential future UAM operations and concepts in both Class C and Class B airspace environments. These simulations have included use of a Langley-developed ADAA research tool called DANTi, which enables configurable ADAA displays to be presented to pilots of simulated eVTOL aircraft participating in higher-density and higher-tempo UAM operations. Experience and observations made during testing of the NASA-developed DANTi ADAA capability in the UAM NFLITE simulation environment will be reported in this paper together with a discussion of airspace integration and regulatory topics.

Detect and Avoid↗