Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “formal”

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 217 records · Page 12

Ultraviolet line profiles of slowly rotating massive star winds using the ‘analytic dynamical magnetosphere’ formalism

Recent large-scale spectropolarimetric surveys have established that a small but significant percentage of massive stars host stable, surface dipolar magnetic fields with strengths on the order of kG. These fields channel the dense, radiatively driven stellar wind into circumstellar magnetospheres, whose density and velocity structure can be probed using ultraviolet (UV) spectroscopy of wind-sensitive resonance lines. Coupled with appropriate magnetosphere models, UV spectroscopy provides a valuable way to investigate the wind–field interaction, and can yield quantitative estimates of the wind parameters of magnetic massive stars. We report a systematic investigation of the formation of UV resonance lines in slowly rotating magnetic massive stars with dynamical magnetospheres. We pair the analytic dynamical magnetosphere (ADM) formalism with a simplified radiative transfer technique to produce synthetic UV line profiles. Using a grid of models, we examine the effect of magnetosphere size, the line strength parameter, and the cooling parameter on the structure and modulation of the line profile. We find that magnetic massive stars uniquely exhibit redshifted absorption at most viewing angles and magnetosphere sizes, and that significant changes to the shape and variation of the line profile with varying line strengths can be explained by examining the individual wind components described in the ADM formalism. Finally, we show that the cooling parameter has a negligible effect on the line profiles.

C Erba↗

A Temporal Differential Dynamic Logic Formal Embedding

Differential dynamic logic is a formal framework to specify and reason about hybrid programs (HPs). The core of dL is a proof calculus that contains a collection of axioms and rules for the rigorous verification of properties of HPs. Recently, dL has been embedded within the theorem prover Prototype Verification System (PVS) resulting in the tool Plaidypvs2. The integration of dL into PVS expands its expressive power; user defined functions, such as trigonometric and other transcendental functions, can be used inside the dL framework, and meta-reasoning about HPs can be performed, including reasoning about entire classes of HPs, specified using dependent types in PVS. The differential temporal dynamic logic (dTL2) extends dL with temporal logic operators to reason about all the states reachable during the execution of an HP. This paper presents a work in progress focusing on embedding dTL2 in PVS as an extension of Plaidypvs. Plaidypvs is expanded with the formalization of a trace semantics for HPs, the definition of the LTL temporal operators eventually and globally, and the implementation of the proof calculus for dTL2. This new embedding has the same capabilties as Plaidypvs, which allows user defined functions and meta-reasoning of properties of HPs. To the best of the authors’ knowledge this is the first implementation of dTL2.

differential dynamic logic↗

A Formal Verification Framework for Runtime Assurance

The simplex architecture is an instance of Runtime Assurance (RTA) where a trusted component takes control of a safety-critical system when an untrusted component violates a safety property. This paper presents a formalization of the simplex RTA framework in the language of hybrid programs. A feature of this formal verification framework is that, for a given system, a specific instantiation can be created and its safety properties are guaranteed by construction. Instantiations may be kept at varying levels of generality, allowing for black box components, such as ML/AI-based controllers, to be modeled. The framework is written in the Prototype Verification System (PVS) using Plaidypvs, an embedding of differential dynamic logic in PVS. As a proof of concept, the framework is illustrated on an automatic vehicle braking system.

Runtime assurance↗

From Formal Errors Towards Realistic Uncertainties

Evaluation of uncertainties of geodetic parameter estimates is the problem that is not yet solved in a satisfactory way. A direct evaluation of the uncertainties derived from a least square solution is labeled "formal" and is usually biased, sometimes up to an order of magnitude. Customary, the use of formal errors for scientific analysis is discouraged. We claim that the root of the problem is neglecting off-diagonal elements in the variance-covariance matrix of the noise in the data. A careful reconstruction of the full variance-covariance matrix, including the off-diagonal terms greatly improves realism of uncertainty estimates derived from least squares. We processed the dataset of VLBI group delays and built a prior variance-covariance of the atmosphere-driven noise based on analysis of the output of NASA high-resolution numerical weather models. We found that the uncertainties of parameter estimates derived from this least square solution that uses such variance-covariance matrices become much closer to realistic errors. We consider approaches for implementation of this method in routine data analysis of space geodesy data.

Leonid Petrov↗

A Formal Verification Framework for Runtime Assurance

The simplex architecture is an instance of Runtime Assurance (RTA) where a trusted component takes control of a safety-critical system when an untrusted component violates a safety property. This paper presents a formalization of the simplex RTA framework in the language of hybrid programs. A feature of this formal verification framework is that, for a given system, a specific instantiation can be created and its safety properties are guaranteed by construction. Instantiations may be kept at varying levels of generality, allowing for black box components, such as ML/AI-based controllers, to be modeled. The framework is written in the Prototype Verification System (PVS) using Plaidypvs, an embedding of differential dynamic logic in PVS. As a proof of concept, the framework is illustrated on an automatic vehicle braking system.

Runtime assurance↗

Results of a Formal Methods Demonstration Project

This paper describes the results of a cooperative study conducted by a team of researchers in formal methods at three NASA Centers to demonstrate FM techniques and to tailor them to critical NASA software systems. This pilot project applied FM to an existing critical software subsystem, the Shuttle's Jet Select subsystem (Phase I of an ongoing study). The present study shows that FM can be used successfully to uncover hidden issues in a highly critical and mature Functional Subsystem Software Requirements (FSSR) specification which are very difficult to discover by traditional means.

formal methods computer system specification compu↗

V and V of Lexical, Syntactic and Semantic Properties for Interactive Systems Through Model Checking of Formal Description of Dialog

During early phases of the development of an interactive system, future system properties are identified (through interaction with end users in the brainstorming and prototyping phase of the application, or by other stakehold-ers) imposing requirements on the final system. They can be specific to the application under development or generic to all applications such as usability principles. Instances of specific properties include visibility of the aircraft altitude, speed… in the cockpit and the continuous possibility of disengaging the autopilot in whatever state the aircraft is. Instances of generic properties include availability of undo (for undoable functions) and availability of a progression bar for functions lasting more than four seconds. While behavioral models of interactive systems using formal description techniques provide complete and unambiguous descriptions of states and state changes, it does not provide explicit representation of the absence or presence of properties. Assessing that the system that has been built is the right system remains a challenge usually met through extensive use and acceptance tests. By the explicit representation of properties and the availability of tools to support checking these properties, it becomes possible to provide developers with means for systematic exploration of the behavioral models and assessment of the presence or absence of these properties. This paper proposes the synergistic use two tools for checking both generic and specific properties of interactive applications: Petshop and Java PathFinder. Petshop is dedicated to the description of interactive system behavior. Java PathFinder is dedicated to the runtime verification of Java applications and as an extension dedicated to User Interfaces. This approach is exemplified on a safety critical application in the area of interactive cockpits for large civil aircrafts.

human-computer interface↗

Towards a Formal Basis for Modular Safety Cases

Safety assurance using argument-based safety cases is an accepted best-practice in many safety-critical sectors. Goal Structuring Notation (GSN), which is widely used for presenting safety arguments graphically, provides a notion of modular arguments to support the goal of incremental certification. Despite the efforts at standardization, GSN remains an informal notation whereas the GSN standard contains appreciable ambiguity especially concerning modular extensions. This, in turn, presents challenges when developing tools and methods to intelligently manipulate modular GSN arguments. This paper develops the elements of a theory of modular safety cases, leveraging our previous work on formalizing GSN arguments. Using example argument structures we highlight some ambiguities arising through the existing guidance, present the intuition underlying the theory, clarify syntax, and address modular arguments, contracts, well-formedness and well-scopedness of modules. Based on this theory, we have a preliminary implementation of modular arguments in our toolset, AdvoCATE.

Safety↗

Formal Verification of the Interaction Between Semi-Algebraic Sets and Real Analytic Functions

Semi-algebraic sets and real analytic functions are fundamental concepts in Real Algebraic Geometry and Real Analysis, respectively. These concepts interact in the study of Differential Equations, where the real analytic solution to a differential equation is known to enter or exit a semi-algebraic set in a predicable way. Motivated to enhance the capability to reason about differential equations in the Prototype Verification System (PVS), a formalization of multivariate polynomials, semi-algebraic sets, and real analytic functions is developed. The favorable way that a real analytic function enters and exits a semi-algebraic set is proven. It is further shown that if the function is assumed to be smooth, a slightly weaker assumption than real analytic, these favorable interactions with semi-algebraic sets may fail.

Real analytic functions↗

Creating Formal Characterizations of Routine Contingency Management in Commercial Aviation

The identification, modelling, and analysis of root causes of accidents and incidents dominate conventional safety management approaches. However, the effect of humans’ safety-producing behavior on the overall resilience of the system is often neglected. Additionally, emerging aviation markets are giving rise to concepts of operation, such as urban air mobility and optionally piloted air cargo operations, that are leading to a shift in locus of control between humans and automation. Without an understanding of the human contribution to safety, it is difficult to assess the effects of these novel role allocations on overall system safety. In this work, safety-producing behaviors are identified and abstracted into resilient performance strategies. Production rules that encapsulate these strategies are then generated and classified in the Soar cognitive architecture. The strategies are then applied to a remotely-operated air cargo example to demonstrate how safe learning is facilitated. The learned rules and strategies are then formally verified.

Safety Critical Systems↗

Reuse of a Formal Model for Requirements Validation

This paper report experience from how a project engaged in the process of requirements analysis for evolutionary builds can reuse the formally specified design model produced for a similar, earlier project in the same domain.

requirements↗

Rapid Application of Lightweight Formal Methods for Consistency Analyses

Lightweight formal methods promise to yield modest analysis results in an extremely rapid manner. To fulfill this promise, they must be able to work with existing information sources, be able to analyze for manifestly desirable properties, be hightly atuomated (especially if dealing with voluminous amounts of information), and able readily customizable and flexible in the face of emerging needs and understanding.

Lightweight↗

Rapid Application of Lightweight Formal Methods for Consistency Analyses

Lightweight formal methods promise to yield modest analysis results in an extremely rapid manner. To fulfill this promise, they must be able to work with existing information sources, be able to analyze for manifestly desirable properties, be highly automated (especially if dealing with voluminous amounts of information), and be readily customizable and flexible in the face of emerging needs and understanding.

Lightweight↗

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↗

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↗

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↗

Formal Methods in the Air

This is an overview of some of the successes of the Formal Methods team at NASA Langley. It includes discussion of the development of the Well-Clear definition for uncrewed aircraft and the subsequent creation of the DAIDALUS Detect and Avoid library, followed by discussion of the team's verification of the Compact Position Reporting algorithm, which led to the development of tools for floating-point analysis.

Formal Methods↗