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 937 records · Page 52
All sourcesNASA NTRSDOE OSTI
NASA NTRS2002

A Rewriting-Based Approach to Trace Analysis

We present a rewriting-based algorithm for efficiently evaluating future time Linear Temporal Logic (LTL) formulae on finite execution traces online. While the standard models of LTL are infinite traces, finite traces appear naturally when testing and/or monitoring red applications that only run for limited time periods. The presented algorithm is implemented in the Maude executable specification language and essentially consists of a set of equations establishing an executable semantics of LTL using a simple formula transforming approach. The algorithm is further improved to build automata on-the-fly from formulae, using memoization. The result is a very efficient and small Maude program that can be used to monitor program executions. We furthermore present an alternative algorithm for synthesizing probably minimal observer finite state machines (or automata) from LTL formulae, which can be used to analyze execution traces without the need for a rewriting system, and can hence be used by observers written in conventional programming languages. The presented work is part of an ambitious runtime verification and monitoring project at NASA Ames, called PATHEXPLORER, and demonstrates that rewriting can be a tractable and attractive means for experimenting and implementing program monitoring logics.

Havelund, Klaus↗
NASA NTRS2003

Tracking and Control of Gas Turbine Engine Component Damage/Life

This paper describes damage mechanisms and the methods of controlling damages to extend the on-wing life of critical gas turbine engine components. Particularly, two types of damage mechanisms are discussed: creep/rupture and thermo-mechanical fatigue. To control these damages and extend the life of engine hot-section components, we have investigated two methodologies to be implemented as additional control logic for the on-board electronic control unit. This new logic, the life-extending control (LEC), interacts with the engine control and monitoring unit and modifies the fuel flow to reduce component damages in a flight mission. The LEC methodologies were demonstrated in a real-time, hardware-in-the-loop simulation. The results show that LEC is not only a new paradigm for engine control design, but also a promising technology for extending the service life of engine components, hence reducing the life cycle cost of the engine.

Jaw, Link C.↗
NASA NTRS2003

Application of Artificial Intelligence Techniques in Unmanned Aerial Vehicle Flight

This paper describes the development of an application of Artificial Intelligence for Unmanned Aerial Vehicle (UAV) control. The project was done as part of the requirements for a class in Artificial Intelligence (AI) at Nova southeastern University and as an adjunct to a project at NASA Goddard Space Flight Center's Wallops Flight Facility for a resilient, robust, and intelligent UAV flight control system. A method is outlined which allows a base level application for applying an AI method, Fuzzy Logic, to aspects of Control Logic for UAV flight. One element of UAV flight, automated altitude hold, has been implemented and preliminary results displayed. A low cost approach was taken using freeware, gnu, software, and demo programs. The focus of this research has been to outline some of the AI techniques used for UAV flight control and discuss some of the tools used to apply AI techniques. The intent is to succeed with the implementation of applying AI techniques to actually control different aspects of the flight of an UAV.

Bauer, Frank H.↗
NASA NTRS2003

Flight Guidance System Requirements Specification

This report describes a requirements specification written in the RSML-e language for the mode logic of a Flight Guidance System of a typical regional jet aircraft. This model was created as one of the first steps in a five-year project sponsored by the NASA Langley Research Center, Rockwell Collins Inc., and the Critical Systems Research Group of the University of Minnesota to develop new methods and tools to improve the safety of avionics designs. This model will be used to demonstrate the application of a variety of methods and techniques, including safety analysis of system and subsystem requirements, verification of key properties using theorem provers and model checkers, identification of potential sources mode confusion in system designs, partitioning of applications based on the criticality of system hazards, and autogeneration of avionics quality code. While this model is representative of the mode logic of a typical regional jet aircraft, it does not describe an actual or planned product. Several aspects of a full Flight Guidance System, such as recovery from failed sensors, have been omitted, and no claims are made regarding the accuracy or completeness of this specification.

Miller, Steven P.↗
NASA NTRS2003

Questions Revisited: A Close Examination of Calculus of Inference and Inquiry

In this paper I examine more closely the way in which probability theory, the calculus of inference, is derived from the Boolean lattice structure of logical assertions ordered by implication. I demonstrate how the duality between the logical conjunction and disjunction in Boolean algebra is lost when deriving the probability calculus. In addition, I look more closely at the other lattice identities to verify that they are satisfied by the probability calculus. Last, I look towards developing the calculus of inquiry demonstrating that there is a sum and product rule for the relevance measure as well as a Bayes theorem. Current difficulties in deriving the complete inquiry calculus will also be discussed.

Knuth, Kevin H.↗
NASA NTRS2003

Deriving Laws from Ordering Relations

It took much effort in the early days of non-Euclidean geometry to break away from the mindset that all spaces are flat and that two distinct parallel lines do not cross. Up to that point, all that was known was Euclidean geometry, and it was difficult to imagine anything else. We have suffered a similar handicap brought on by the enormous relevance of Boolean algebra to the problems of our age-logic and set theory. Previously, I demonstrated that the algebra of questions is not Boolean, but rather is described by the free distributive algebra. To get to this stage took much effort, as many obstacles-most self-placed-had to be overcome. As Boolean algebras were all I had ever known, it was almost impossible for me to imagine working with an algebra where elements do not have complements. With this realization, it became very clear that the sum and product rules of probability theory at the most basic level had absolutely nothing to do with the Boolean algebra of logical statements. Instead, a measure of degree of inclusion can be invented for many different partially ordered sets, and the sum and product rules fall out of the associativity and distributivity of the algebra. To reinforce this very important idea, this paper will go over how these constructions are made, while focusing on the underlying assumptions. I will derive the sum and product rules for a distributive lattice in general and demonstrate how this leads to probability theory on the Boolean lattice and is related to the calculus of quantum mechanical amplitudes on the partially ordered set of experimental setups. I will also discuss the rules that can be derived from modular lattices and their relevance to the cross-ratio of projective geometry.

Knuth, Kevin H.↗
NASA NTRS2003

Discrete Abstractions of Hybrid Systems: Verification of Safety and Application to User-Interface Design

Human interaction with a complex control system involves the user, the automation’s discrete mode logic, and the underlying continuous dynamics of the physical system. The user-interface of such systems always displays a reduced set of information about the entire system. Designing interfaces such that all the pertinent information is available and assuring that this information is correct is important for any user-interface, but especially so for safety-critical systems such as automotive systems and autopilots. Here we describe a methodology for the analysis of hybrid control systems that incorporate user interaction, with the goal of assuring that the information provided to the user is correct. That is, the user-interface must contain all information necessary to safely complete a desired procedure or task. We begin with a hybrid system model which incorporates discrete mode logic as well as nonlinear continuous dynamics. Using a hybrid computational tool for reachability, we find the largest region of the state-space in which we can guarantee the state of the system can always remain – this is the safe region of operation. By implementing a controller for safety which arises from this computation, we mathematically guarantee that this safe region is invariant, meaning that the system will always remain within the safe region if the determined controller is used on the boundary of the safe region. Verification within a hybrid framework allows us to account for the continuous dynamics underlying the discrete representations displayed to the user. Using the computed invariant regions as discrete states, we can abstract a discrete event system from this hybrid system with safety restrictions. This abstraction can be used to determine what information must be provided on the display. Furthermore, in cases in which an interface already exists, the abstraction provides the necessary input into existing interface verification methods. We provide two examples: a car traveling through a yellow light at an intersection and an aircraft autopilot in an automatic landing/go-around maneuver. The examples demonstrate the applicability of this methodology to hybrid systems that have operational constraints we can pose in terms of safety. This methodology differs from existing work in hybrid system verification in that we directly account for the user’s interactions with the system.

Meeko Oishi↗
NASA NTRS2004

Product-oriented Software Certification Process for Software Synthesis

The purpose of this document is to propose a product-oriented software certification process to facilitate use of software synthesis and formal methods. Why is such a process needed? Currently, software is tested until deemed bug-free rather than proving that certain software properties exist. This approach has worked well in most cases, but unfortunately, deaths still occur due to software failure. Using formal methods (techniques from logic and discrete mathematics like set theory, automata theory and formal logic as opposed to continuous mathematics like calculus) and software synthesis, it is possible to reduce this risk by proving certain software properties. Additionally, software synthesis makes it possible to automate some phases of the traditional software development life cycle resulting in a more streamlined and accurate development process.

Nelson, Stacy↗
NASA NTRS2003

Application of Artificial Intelligence Techniques in Uninhabitated Aerial Vehicle Flight

This paper describes the development of an application of Artificial Intelligence (AI) for Unmanned Aerial Vehicle (UAV) control. The project was done as part of the requirements for a class in AI at NOVA southeastern University and a beginning project at NASA Wallops Flight Facility for a resilient, robust, and intelligent UAV flight control system. A method is outlined which allows a base level application for applying an Artificial Intelligence method, Fuzzy Logic, to aspects of Control Logic for UAV flight. One element of UAV flight, automated altitude hold, has been implemented and preliminary results displayed.

Dufrene, Warren R., Jr.↗
NASA NTRS2004

Field Effect Transistor Behavior in Electrospun Polyaniline/Polyethylene Oxide Nanofibers

Novel translators and logic devices based on nanotechnology concepts are under intense development. The potential for ultra-low power circuitry makes nanotechnology attractive for applications such as digital electronics and sensors. Furthermore, the ability to form devices on flexible substrates expands the range of applications where electronic circuitry can be introduced. For NASA, nonotechndogy offers opportunities for increased onboard data processing and thus autonomous decision-making ability, ad novel sensors that detect and respond to external stimuli with few oversight requirements. The goat of this work is to demonstrate transistor behavior in polyaniline/ polyethylene oxide nanofibers, thus creating a foundation for future logic devices.

Miranda, Felix A.↗
NASA NTRS2004

Application of Artificial Intelligence Techniques in Uninhabited Aerial Vehicle Flight

This paper describes the development of an application of Artificial Intelligence (AI) for Unmanned Aerial Vehicle (UAV) control. The project was done as part of the requirements for a class in AI at NOVA Southeastearn University and a beginning project at NASA Wallops Flight Facility for a resilient, robust, and intelligent UAV flight control system. A method is outlined which allows a base level application for applying an Artificial Intelligence method, Fuzzy Logic, to aspects of Control Logic for UAV flight. One element of UAV flight, automated altitude hold, has been implemented and preliminary results displayed.

Dufrene, Warren R., Jr.↗
NASA NTRS2003

NASA/BAE SYSTEMS SpaceWire Effort

This paper discusses the state of the NASA and BAE SYSTEMS developments of SpaceWire. NASA has developed intellectual property that implements SpaceWire in Register Transfer Level (RTL) VHDL for a SpaceWire link and router. This design has been extensively verified using directed tests from the SpaceWire Standard and design specification, as well as being randomly tested to flush out hard to find bugs in the code. The high level features of the design will be discussed, including the support for multiple time code masters, which will be useful for the James Webb Space Telescope electrical architecture. This design is now ready to be targeted to FPGA's and ASICs. Target utilization and performance information will be presented for Spaceflight worthy FPGA's and a discussion of the ASIC implementations will be addressed. In particular, the BAE SYSTEMS ASIC will be highlighted which will be implemented on their .25micron rad-hard line. The chip will implement a 4-port router with the ability to tie chips together to make larger routers without external glue logic. This part will have integrated LVDS drivers/receivers, include a PLL and include skew control logic. It will be targeted to run at greater than 300 MHz and include the implementation for the proposed SpaceWire transport layer. The need to provide a reliable transport mechanism for SpaceWire has been identified by both NASA And ESA, who are attempting to define a transport layer standard that utilizes a low overhead, low latency connection oriented approach that works end-to-end. This layer needs to be implemented in hardware to prevent bottlenecks.

Rakow, Glenn Parker↗
NASA NTRS2003

NASA/BAE Systems SpaceWire Efforts

This paper discusses the state of the NASA and BAE SYSTEMS developments using Spacewire. NASA has developed intellectual property that implements Spacewire in Register Transfer Level VHDL for a Spacewire link and router. This design has been extensively verified using directed tests from the Spacewire Standard and design specification, as well as being randomly tested to flush out hard to find bugs in the code. The high level features of the design will be discussed, including the support for multiple time code masters, which will be useful for the James Webb Space Telescope electrical architecture. This design is now ready to be targeted to FPGA's and ASICs. Target utilization and performance information will be presented for some spaceflight qualified FPGA's and a discussion of the ASIC implementations will be addressed. In particular, the BAE SYSTEMS ASIC will be highlighted which will be implemented in their 0.25 micron rad-hard line. The chip will implement a 4-port router with the ability to tie chips together to make larger routers without external glue logic. This part will have integrated LVDS driver/receivers, include a PLL and include skew control logic. It will be targeted to run at greater than 300 MHz and include the implementation for the proposed Spacewire transport layer. The need to provide a reliable transport mechanism for Spacewire has been identified by both NASA and ESA, who are attempting to define a transport layer standard that utilizes a low overhead, low latency connection oriented approach. The Transport layer needs to be implemented in hardware-to prevent bottlenecks.

Rakow, Glenn Parker↗
NASA NTRS2004

A Multi-Discipline, Multi-Genre Digital Library for Research and Education

We describe NCSTRL+, a unified, canonical digital library for educational and scientific and technical information (STI). NCSTRL+ is based on the Networked Computer Science Technical Report Library (NCSTRL), a World Wide Web (WWW) accessible digital library (DL) that provides access to over 100 university departments and laboratories. NCSTRL+ implements two new technologies: cluster functionality and publishing "buckets". We have extended the Dienst protocol, the protocol underlying NCSTRL, to provide the ability to "cluster" independent collections into a logically centralized digital library based upon subject category classification, type of organization, and genres of material. The concept of "buckets" provides a mechanism for publishing and managing logically linked entities with multiple data formats. The NCSTRL+ prototype DL contains the holdings of NCSTRL and the NASA Technical Report Server (NTRS). The prototype demonstrates the feasibility of publishing into a multi-cluster DL, searching across clusters, and storing and presenting buckets of information.

Nelson, Michael L.↗
NASA NTRS1998

NCSTRL+: Adding Multi-Discipline and Multi-Genre Support to the Dienst Protocol Using Clusters and Buckets

We describe NCSTRL+, a unified, canonical digital library for scientific and technical information (STI). NCSTRL+ is based on the Networked Computer Science Technical Report Library (NCSTRL), a World Wide Web (WWW) accessible digital library (DL) that provides access to over 100 university departments and laboratories. NCSTRL+ implements two new technologies: cluster functionality and publishing buckets. We have extended Dienst, the protocol underlying NCSTRL, to provide the ability to cluster independent collections into a logically centralized digital library based upon subject category classification, type of organization, and genres of material. The bucket construct provides a mechanism for publishing and managing logically linked entities with multiple data forms as a single object. The NCSTRL+ prototype DL contains the holdings of NCSTRL and the NASA Technical Report Server (NTRS). The prototype demonstrates the feasibility of publishing into a multi-cluster DL, searching across clusters, and storing and presenting buckets of information.

Nelson, Michael L.↗
NASA NTRS2004

Virtex-II Pro SEE Test Methods and Results

The Xilinx Virtex-II Pro is a platform FPGA that embeds multiple microprocessors within the fabric of an SRAM-based reprogrammable FPGA. The variety and quantity of resources provided by this family of devices make them very attractive for spaceflight applications. However, these devices will be susceptible to single event effects (SEE), which must be mitigated. To use the Virtex-II Pro reliably in space applications, these devices must first be tested to determine if they are susceptible to single event latchup (SEL), the degree to which they are susceptible to single event upsets (SEU) and single event transients (SET), and how these effects are manifested in the device. With this information, mitigations schemes can be developed and tested that address the specific susceptiblities of these devices. This initial SEE test uses a commercial off the shelf Virtex-II Pro evaluation board, with a single processor XC2VP7 FPGA. The FPGA on this board is an acid etched device, which can be partially covered with a shield. The shield covers a portion of the logic, routing, and memory resources along with some of the RocketIO transceivers. The processor, along with a large portion of logic, routing, memory, and transceivers are left exposed. This test will be performed at the Cyclotron Laboratories at Texas A&M University and Michigan State University using ions of varying energy levels and fluencies.

Petrick, David↗
NASA NTRS2004

Formalization of the Integral Calculus in the PVS Theorem Prover

The PVS Theorem prover is a widely used formal verification tool used for the analysis of safety-critical systems. The PVS prover, though fully equipped to support deduction in a very general logic framework, namely higher-order logic, it must nevertheless, be augmented with the definitions and associated theorems for every branch of mathematics and Computer Science that is used in a verification. This is a formidable task, ultimately requiring the contributions of researchers and developers all over the world. This paper reports on the formalization of the integral calculus in the PVS theorem prover. All of the basic definitions and theorems covered in a first course on integral calculus have been completed.The theory and proofs were based on Rosenlicht's classic text on real analysis and follow the traditional epsilon-delta method. The goal of this work was to provide a practical set of PVS theories that could be used for verification of hybrid systems that arise in air traffic management systems and other aerospace applications. All of the basic linearity, integrability, boundedness, and continuity properties of the integral calculus were proved. The work culminated in the proof of the Fundamental Theorem Of Calculus. There is a brief discussion about why mechanically checked proofs are so much longer than standard mathematics textbook proofs.

Butler, Ricky W.↗
NASA NTRS2004

Meeting the Deadline: Why, When and How

A normative system is defined as any set of interacting agents whose behavior can usefully be regarded as norm-directed. Most organizations, and more specifically institutions, fall under this definition. Interactions in these normative systems are regulated by normative templates that describe desired behavior in terms of deontic concepts (obligations, prohibitions and permissions), deadlines, violations and sanctions. Agreements between agents, and between an agent and the society, can then be specified by means of contracts. Contracts provide flexible but verifiable means to integrate society requirements and agent autonomy. and are an adequate means for the explicit specification of interactions. From the society perspective, it is important that these contracts adhere to the specifications described in the model of the organization. If we want to automate such verifications, we have to formalize the languages used for contracts and for the specification of organizations. The logic LCR is based on deontic temporal logic. LCR is an expressive language for describing interaction in multi-agent systems, including obligations with deadlines. Deadlines are important norms in most interactions between agents. Intuitively, a deadline states that an agent should perform an action before a certain point in time. The obligation to perform the action starts at the moment the deadline becomes active. E.g. when a contract is signed or approved. If the action is not performed in time a violation of the deadline occurs. It can be specified independently what measure has to be taken in this case. In this paper we investigate the deadline concept in more detail. The paper is organized as follows. Section 2 defines the variant of CTL we use. In section 3, we discuss the basic intuitions of deadlines. Section 4 presents a first intuitive formalization for deadlines. In section 5, we look at a more complex model for deadlines trying to catch some more practical aspects. Finally, in section 6 we present issues for future work and our conciusions.

Dignum, Frank↗