Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “logic”

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 703 records · Page 39
All sourcesNASA NTRSDOE OSTI
NASA NTRS2012

mREST Interface Specification

mREST is an implementation of the REST architecture specific to the management and sharing of data in a system of logical elements. The purpose of this document is to clearly define the mREST interface protocol. The interface protocol covers all of the interaction between mREST clients and mREST servers. System-level requirements are not specifically addressed. In an mREST system, there are typically some backend interfaces between a Logical System Element (LSE) and the associated hardware/software system. For example, a network camera LSE would have a backend interface to the camera itself. These interfaces are specific to each type of LSE and are not covered in this document. There are also frontend interfaces that may exist in certain mREST manager applications. For example, an electronic procedure execution application may have a specialized interface for configuring the procedures. This interface would be application specific and outside of this document scope. mREST is intended to be a generic protocol which can be used in a wide variety of applications. A few scenarios are discussed to provide additional clarity but, in general, application-specific implementations of mREST are not specifically addressed. In short, this document is intended to provide all of the information necessary for an application developer to create mREST interface agents. This includes both mREST clients (mREST manager applications) and mREST servers (logical system elements, or LSEs).

McCartney, Patrick↗
NASA NTRS2014

Using a Commercial Ethernet PHY Device in a Radiation Environment

This work involved placing a commercial Ethernet PHY on its own power boundary, with limited current supply, and providing detection methods to determine when the device is not operating and when it needs either a reset or power-cycle. The device must be radiation-tested and free of destructive latchup errors. The commercial Ethernet PHY's own power boundary must be supplied by a current-limited power regulator that must have an enable (for power cycling), and its maximum power output must not exceed the PHY's input requirements, thus preventing damage to the device. A regulator with configurable output limits and short-circuit protection (such as the RHFL4913, rad hard positive voltage regulator family) is ideal. This will prevent a catastrophic failure due to radiation (such as a short between the commercial device's power and ground) from taking down the board's main power. Logic provided on the board will detect errors in the PHY. An FPGA (field-programmable gate array) with embedded Ethernet MAC (Media Access Control) will work well. The error detection includes monitoring the PHY's interrupt line, and the status of the Ethernet's switched power. When the PHY is determined to be non-functional, the logic device resets the PHY, which will often clear radiation induced errors. If this doesn't work, the logic device power-cycles the FPGA by toggling the regulator's enable input. This should clear almost all radiation induced errors provided the device is not latched up.

Parks, Jeremy↗
NASA NTRS2013

The Integration of DCS I/O to an Existing PLC

At the NASA Glenn Research Center (GRC), Existing Programmable Logic Controller (PLC) I/O was replaced with Distributed Control System (DCS) I/O, while keeping the existing PLC sequence Logic. The reason for integration of the PLC logic and DCS I/O, along with the evaluation of the resulting system is the subject of this paper. The pros and cons of the old system and new upgrade are described, including operator workstation screen update times. Detail of the physical layout and the communication between the PLC, the DCS I/O and the operator workstations are illustrated. The complex characteristics of a central process control system and the plan to remove the PLC processors in future upgrades is also discussed.

Sadhukhan, Debashis↗
NASA NTRS2014

Data Automata in Scala

The field of runtime verification has during the last decade seen a multitude of systems for monitoring event sequences (traces) emitted by a running system. The objective is to ensure correctness of a system by checking its execution traces against formal specifications representing requirements. A special challenge is data parameterized events, where monitors have to keep track of the combination of control states as well as data constraints, relating events and the data they carry across time points. This poses a challenge wrt. efficiency of monitors, as well as expressiveness of logics. Data automata is a form of automata where states are parameterized with data, supporting monitoring of data parameterized events. We describe the full details of a very simple API in the Scala programming language, an internal DSL (Domain-Specific Language), implementing data automata. The small implementation suggests a design pattern. Data automata allow transition conditions to refer to other states than the source state, and allow target states of transitions to be inlined, offering a temporal logic flavored notation. An embedding of a logic in a high-level language like Scala in addition allows monitors to be programmed using all of Scala's language constructs, offering the full flexibility of a programming language. The framework is demonstrated on an XML processing scenario previously addressed in related work.

runtime verification↗
NASA NTRS2019

Unmanned Aircraft Systems (UAS) Integration in the National Airspace System (NAS) Project: ACAS Xu HITL Overview

This presentation provides an overview of a recently completed human-in-the-loop simulation, conducted as part of the Unmanned Aircraft Systems (UAS) Integration in the National Airspace System (NAS) Project. This study examined how to present resolution advisories (RAs) issued by Airborne Collision Avoidance System (ACAS) Xu, which can be in the vertical dimension, the horizontal dimension, or both (i.e., "blended"). The study varied the location of the ACAS Xu traffic information - it was either presented within an 'integrated' display or a 'standalone' display, where the traffic information was separated from the vehicle control interfaces and navigational information. The presentation covers the test set-up, scenario design, and facilities utilized in this experiment. The primary dependent variables are listed, but no detailed results are included in this outbrief since data analysis is still underway. Goal: assess ACAS Xu Run 5 in a HITL setting to measure pilot & system performance – RWC alerting and guidance – RA alerting and guidance • Horizontal-only, vertical-only, and blended RAs • Strengthening RAs, reversals and added/removed RAs during blended maneuvers – Incorporate realistic sensor noise into the simulation environment – Compare pilot and DAA system performance back to NASA’s Phase 1 DAA MOPS V&V HITL • We leveraged the findings of an engineering analysis conducted in March to help inform how to implement the Xu logic – Part 1 focused on how to display horizontal-only, vertical-only and blended RAs – Part 2 focused on how to display automated RA responses Xu Engineering Analysis Results Part 1 objectives: – Characterize pilot responses to (canned) ACAS Xu RAs in a variety of display configurations • With vs. Without text accompaniment • Simple vs. ‘Advanced’ aural alerting • Results – Pilots struggled to meet 5 seconds initial response requirement • Particularly against horizontal and blended RAs – Pilots failed to respond more quickly to secondary RAs • Expected response time to subsequent RAs = 2.5 seconds No clear effect of the different alerting conditions on response times – Response times primarily driven by RA type • Pilots demonstrated high level of compliance with RAs and self-reported Xu alerting and guidance as being acceptable – 1/5 reported text as being necessary – 4/5 wanted the aural alert to retain the original RA sequence (i.e., issue a follow-on RA second rather than first) – 4/5 wanted to retain the “Maintain Heading/Vertical Speed” aural alert in the event that the pilot reached their target response at the time of secondary RA Based on these results, we decided on the following for the HITL experimental design: – Incorporated an ‘auto-fill’ feature in Vigilant Spirit that removes the need for pilots to manually enter a heading or altitude for RAs • Pilots only have to click ‘Send’ to upload the RA target heading/altitude – Did not include an RA ‘text box’ • The auto-fill feature largely replaces the purpose of the text box – Using a combination of the ‘Basic’ and ‘Advanced’ aural alerting • In case of blended maneuvers will issue “Maintain Heading/Vertical Rate” if pilot has reached 1st RA target at the time the 2nd RA is issued • Integration and testing with Xu Run 5 also resulted in us adding display logic to modify how horizontal RAs are presented – Target heading was shown to update at approx. 1 Hz making it difficult for pilots to implement – Display logic limited horizontal RA strengthening to once every 5 seconds • Did not impact timing of reversals, new RAs (i.e., blended), or CoC Engineering Analysis Results

human systems integration↗
NASA NTRS2010

TPSAS-NF1676L-9990-DND

PVS (Prototype Veri cation System)1 is an interactive environment for the specification and verification of systems. PVS provides a strongly typed specification language, which is based on Higher-Order Logic. The type system of PVS supports: sub-typing, dependent-types, abstract data types, parametric types, records, unions, and tuples. The PVS theorem prover includes decision procedures for a variety of theories such as linear arithmetic, propositional logic, and temporal logic. This seminar will provide a gentle introduction to the basic and advanced features of PVS, including: theory interpretations, real number proving, batch proving, rapid prototyping, and strategy development. All these features are illustrated with simple examples and exercises.

César Muñoz↗
NASA NTRS2018

Efficient Runtime Verification of First-Order Temporal Properties

Runtime verification allows monitoring the execution of a system against a temporal property, raising an alarm if the property is violated. In this paper we present a theory and system for runtime verification of a first-order past time linear temporal logic. The first-order nature of the logic allows a monitor to reason about events with data elements. While runtime verification of propositional temporal logic requires only a fixed amount of memory, the first-order variant has to deal with a number of data values potentially growing unbounded in the length of the execution trace. This requires special compactness considerations in order to allow checking very long executions. In previous work we presented an efficient use of BDDs for such first-order runtime verification, implemented in the tool DEJAVU. We first summarize this previous work. Subsequently, we look at the new problem of dynamically identifying when data observed in the past are no longer needed, allowing to reclaim the data elements used to represent them. We also study the problem of adding relations over data values. Finally, we present parts of the implementation, including a new concept of user defined property macros.

Peled, Doron↗
NASA NTRSDate not supplied

Minimum-Violation Traffic Management for Urban Air Mobility

Urban air mobility (UAM) refers to air transportation services in and over an urban area and has the potential to revolutionize mobility solutions. However, due to the projected scale of operations, current air traffic management (ATM) techniques are not viable. Increasingly autonomous systems are a pathway to accelerate the realization of UAM operations but must be fielded safely and efficiently. The heavily regulated, safety critical nature of aviation may lead to multiple, competing safety constraints that can be traded off based on the operational context. In this paper, we design a framework which allows for the scalable planning of a UAM ATM system. We formalize safety oriented constraints derived from FAA regulations by encoding them as temporal logic formulae. We then propose a method for UAM ATM that is both scalable and minimally violates the temporal logic constraints. Numerical results show that the runtime for our proposed algorithm is suitable for very large problems and is backed by theoretical guarantees of correctness with respect to given temporal logic constraints.

Urban Air Mobility↗
NASA NTRSDate not supplied

Applying Formal Methods to Safety-Critical Systems

How do you know a proof is correct? Traditionally, mathematical proofs are socially verified – at least one human, following a set of implicit rules of natural language and logic, determines if the proof is believable. If the proof becomes overly tedious and/or is essential to some safety- or mission-critical application, it becomes necessary to determine the soundness to a higher standard. 'Formal methods' refer to mathematically rigorous techniques and tools that enable specification, design, and verification of hardware and software systems. The specification used in formal methods are statements in a mathematical logic while the formal verifications are deductions in that logic. Formal methods can be difficult or time/resource intensive, but offer a higher level of assurance than standard verification through testing or handwritten proofs. This talk will introduce formal methods, motivated by applications of interest to NASA, including uncrewed aircraft operations in the national airspace, urban air environments, and wildfire areas. The audience will be given a crash course in mechanically verified proofs in the Prototype Verification System (PVS), an interactive theorem prover.

Formal Methods↗
NASA NTRSDate not supplied

Floquet Codes on Non-Trivalent Lattices

Floquet codes are a novel form of quantum error correcting codes, where the logical degrees of freedom appear in a dynamical form. The first example of such a code was constructed by Hastings and Haah on a honeycomb lattice. Specifically, they showed how to Floquetify the Kitaev honeycomb model, which when viewed as a subsystem code, encodes no logical qubits. However, by choosing a particular measurement schedule of the check operators, this model leads to dynamically encoded logical qubits. Since this initial work, several examples of Floquet codes have been constructed, mainly on trivalent lattices. Here, we report progress on understanding when such codes can be implemented on lattices of different connectivities.

Muhammad Sohaib Alam↗
NASA NTRS2006

New Challenges in Model Checking

In the last 25 years, the notion of performing software verification with logic model checking techniques has evolved from intellectual curiosity to accepted technology with significant potential for broad practical application. In this paper we look back at the main steps in this evolution and illustrate how the challenges have changed over the years, as we sharpened our theories and tools. Next we discuss a typical challenge in software verification that we face today - and that perhaps we can look back on in another 25 years as having inspired the next logical step towards a broader integration of model checking into the software development process.

software verification↗
NASA NTRSDate not supplied

Lessons Learned from NASA Goddard Space Flight Center’s Product Development Lead Training Schedule and Cost Development Workshop: Continuous Improvement

This presentation provides a status of the Goddard Space Flight Center (GSFC) effort to increase foundational knowledge of Product Development Leads (PDLs) in schedule and cost management including earned value management (EVM). In 2012, GSFC’s Engineering and Technology Directorate (ETD) implemented an in-house training program to prepare PDLs for managing the technical, cost, schedule, and risk aspects of spaceflight systems to meet their subsystem commitments. Developed in-house, the PDL training program provides an integrated approach to requirements development, risk, schedule and cost management, EVM, performance tracking, and other areas. The program has been held twice yearly since its inception with 531 participating and 451 completing the curriculum. In 2017, the program won the Robert H. Goddard award for Quality and Process Improvement. Program development and evolution were presented in the 2018 NASA Schedule and Cost Symposium. The presentation was so well received that this year we focus on one workshop within the program: Schedule and Cost Development, including EVM. We examine the on-going logic modeling process and how participant and stakeholder data influence workshop content and design, and how the disciplines of schedule and cost contribute to mission success. In this presentation we refresh you on how the approach integrates lecture, small group discussion, estimating, case study exercises, and problem solving. We update you on the data collected from participants and stakeholders, and we discuss how we use these data to measure training effectiveness. Specific topics include: • How the logic model is used as the backbone for continuous program improvement, • How feedback influences implementation and curriculum updates, • How data collection and analysis inform workshop content and development, including participant discoveries of EVM data, • How including the resource analyst and planner in the product development team supports project success.

Lessons Learned↗
NASA NTRSDate not supplied

Verifying PLC Programs via Monitors: Extending the Integration of FRET and PLCverif

Verification of Programmable Logic Controller (PLC) programs requires reasoning about propositions qualified in terms of time. CERN’s PLCverif, an open-source tool for the analysis of safety-critical PLC systems, uses Linear Temporal Logic (LTL) for the specification of properties. Until now, PLCverif depended on third-party tools that accept LTL specifications to perform verification. However, our experience with industrial PLC programs shows that, to overcome analysis limitations, a wide range of techniques are needed to successfully verify complex properties. In this paper, we extend PLCverif to enable PLC program verification of pure-past LTL (PLTL) safety properties with assertion-based verification tools. To this end, we take an algorithm from the runtime-monitoring domain, apply it to bounded model checking of PLC programs, and implement it in PLCverif. We extend the integration of NASA’s Formal Requirements Elicitation Tool (FRET) into PLCverif to use PLTL properties generated with FRET. In addition, we leverage the program structure induced by the PLC scan-cycle for a state-space reduction. Finally, we expose the algorithm to a real-world case study of critical systems at CERN.

Formal verification↗
NASA NTRS1966

Digital system provides superregulation of nanosecond amplifier-discriminator circuit

Feedback system employing a digital logic comparator to detect and correct amplifier drift provides stable gain characteristics for nanosecond amplifiers used in counting applications. Additional anticoincidence logic enables application of the regulation circuit to the amplifier and discriminator while they are mounted in an operable circuit.

Forges, K. G.↗
NASA NTRS1969

Self-starting circuit for switching regulators

Schematic is provided on a self-starting circuit for a switching regulator which uses a logic circuit to sense a change in output voltage and provides a correction signal for dc power sources. With this device, the total power consumed by the logic circuitry is held to a minimum, and the circuit receives the optimum regulated supply power.

Schraut, E. H.↗